# Validate proof for $A \Rightarrow B, (C \vee \neg A) \Rightarrow F, B \Rightarrow D, \neg D \vDash F$

I have the following premises:

$$A \Rightarrow B, (C \vee \neg A) \Rightarrow F, B \Rightarrow D, \neg D$$

I attempted to construct a proof for the conclusion $$F$$ using inference rules, but I'm not sure if my proof is correct. Here is the proof I came up with:

1. $$B \Rightarrow D$$: Premise 1 (P1)
2. $$\neg D$$: Premise 2 (P2)
3. $$\neg B$$: Modus tollens on P1 and P2
4. $$A \Rightarrow B$$: Premise 3 (P3)
5. $$\neg A$$: Modus tollens on 3. and P3
6. $$(C \vee \neg A) \Rightarrow F$$: Premise 4 (P4)
7. $$\neg (C \vee \neg A) \vee F$$: Implication elimination in 6.
8. $$(\neg C \wedge \neg \neg A) \vee F$$ DeMorgan Law
9. $$(\neg C \wedge A) \vee F$$ : Double negation in 8.
10. $$F \vee (\neg C \wedge A)$$ : Commutativity law
11. $$(F \vee A) \wedge (F \vee \neg C)$$ : Distributivity law
12. $$F \vee A$$ & $$\wedge$$-elimination through simplification rule
13. $$F$$: Disjunctive syllogism of 12. and 5. $$(\neg A)$$
14. $$F$$: Conclusion

Is this proof correct?

Any suggestions or corrections would be appreciated!

• How about you say anywhere up front what you are trying to prove. It makes it a lot easier to read a proof if you know the goal. And the title is wrong - the proof is not "of" the premises. Commented May 19 at 10:57
• Maybe after step 5 Addition will be useful: from $\lnot A$ to $C \lor \lnot A$. Commented May 19 at 13:02
• Note that technically, your proof should be a semantic one since you use $\vDash$ as opposed to $\vdash$. Otherwise, it looks fine. Commented May 19 at 16:38