Theorem not12an2impnot1

Description: If a double conjunction is false and the second conjunct is true, then the first conjunct is false. https://us.metamath.org/other/completeusersproof/not12an2impnot1vd.html is the Virtual Deduction proof verified by automatically transforming it into the Metamath proof of not12an2impnot1 using completeusersproof, which is verified by the Metamath program. https://us.metamath.org/other/completeusersproof/not12an2impnot1ro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 13-Jun-2018)

	Ref	Expression
Assertion	not12an2impnot1	$$⊢\left(\neg \left(\phi \wedge \psi \right)\wedge \psi \right)\to \neg \phi$$

Proof

Step	Hyp	Ref	Expression
1		pm3.21	$$⊢\psi \to \left(\phi \to \left(\phi \wedge \psi \right)\right)$$
2	1	con3rr3	$$⊢\neg \left(\phi \wedge \psi \right)\to \left(\psi \to \neg \phi \right)$$
3	2	imp	$$⊢\left(\neg \left(\phi \wedge \psi \right)\wedge \psi \right)\to \neg \phi$$