Exercise logic.propositional.consequence

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

Derivation

(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