Derivation of F from ¬E V F and ¬E -> F

Question

I want to derive F from ¬E V F and ¬E -> F

Here is what I have done:

1. ¬E -> F // hyp
2. ¬E V F // hyp
3. ¬E // AA
4. F // E ->(2)
5. F // AA

6. ¬F  //   AA
   

7. F // E ¬(6)
8. F // Ev(2-4,5-7)

I don't know if I can assume ¬F like in 6 and deduce that I have F because there is a contradiction, Is it a good writing ?

Answer 1

You can end the proof on line $5$ citing disjunction-elimination "$\vee$E"

For instance...

$ \neg E \vee F, \neg E \to F \vdash F $

$\{1\} \:\:\:\:\:\:\:\:1. \neg E \vee F \:\:\:\:\:\:\:$ premise

$\{2\} \:\:\:\:\:\:\:\: 2. \neg E \to F \:\:\:\:\:\:$ premise

$\{3\} \:\:\:\:\:\:\:\: 3. \neg E \:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:$ Assumption

$\{2,3\} \:\:\:\: 4. F \:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:$ $2,3$ Modus Ponens

$\{5\} \:\:\:\:\:\:\:\: 5. F \:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:$ Assumption

$\{1,2\} \:\:\:\: 6. F \:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:$ $1, 3, 4, 5, 5$ Disjunction-Elimination

Notice on line $5$ you are able to conclude the very thing you assume, completing the second derivation needed for $\vee$E