Exercise logic.propositional.consequence

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

Derivation

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

⇒ logic.propositional.defimpl

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

⇒ logic.propositional.notnot

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

⇒ fakeabsorption

p /\ q => p

⇒ conj-elim

p => p