Exercise logic.propositional.consequence

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

Derivation

p -> (q -> r), q => p -> r

⇒ conj-intro, initial=TList [TCon logic1.implies [TVar "p",TCon logic1.implies [TVar "q",TVar "r"]],TVar "q"]

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

⇒ logic.propositional.defimpl

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

⇒ logic.propositional.defimpl

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

⇒ logic.propositional.defimpl

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

⇒ fakeabsorption

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

⇒ conj-elim

~p || r => ~p || r