Exercise logic.propositional.consequence

Description
Prove that formula is a logical consequence of a set of formulas

Derivation

q => p -> (p /\ q)

⇒ logic.propositional.defimpl, initial=TList [TVar "q"]

q => ~p || (p /\ q)

⇒ logic.propositional.oroverand

q => (~p || p) /\ (~p || q)

⇒ logic.propositional.complor

q => T /\ (~p || q)

⇒ logic.propositional.truezeroand

q => ~p || q

⇒ introfalseleft

F || q => ~p || q

⇒ introcompl

(p /\ ~p) || q => ~p || q

⇒ logic.propositional.oroverand

(p || q) /\ (~p || q) => ~p || q

⇒ conj-elim

~p || q => ~p || q