Exercise logic.propositional.consequence
Description
Prove that formula is a logical consequence of a set of formulas
Derivation
![](http://ideas.cs.uu.nl/images/external.png)
~q => (~p /\ ~q) || p
⇒ logic.propositional.oroverand~q => (~p || p) /\ (~q || p)
⇒ logic.propositional.complor~q => T /\ (~q || p)
⇒ logic.propositional.truezeroand~q => ~q || p
⇒ commor.sort~q => p || ~q
⇒ introfalseleftF || ~q => p || ~q
⇒ introcompl(p /\ ~p) || ~q => p || ~q
⇒ logic.propositional.oroverand(p || ~q) /\ (~p || ~q) => p || ~q
⇒ conj-elimp || ~q => p || ~q