Exercise logic.propositional.consequence
Description
Prove that formula is a logical consequence of a set of formulas
Derivation
(p -> q) /\ (p -> ~q) => ~p
⇒ logic.propositional.defimpl(~p || q) /\ (p -> ~q) => ~p
⇒ logic.propositional.defimpl(~p || q) /\ (~p || ~q) => ~p
⇒ introfalseleft(~p || q) /\ (~p || ~q) => F || ~p
⇒ introcompl(~p || q) /\ (~p || ~q) => (q /\ ~q) || ~p
⇒ logic.propositional.oroverand(~p || q) /\ (~p || ~q) => (q || ~p) /\ (~q || ~p)
⇒ commor.sort(~p || q) /\ (~p || ~q) => (~p || q) /\ (~q || ~p)
⇒ commor.sort(~p || q) /\ (~p || ~q) => (~p || q) /\ (~p || ~q)