Metamath Proof Explorer


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 ( ( ¬ ( 𝜑𝜓 ) ∧ 𝜓 ) → ¬ 𝜑 )

Proof

Step Hyp Ref Expression
1 pm3.21 ( 𝜓 → ( 𝜑 → ( 𝜑𝜓 ) ) )
2 1 con3rr3 ( ¬ ( 𝜑𝜓 ) → ( 𝜓 → ¬ 𝜑 ) )
3 2 imp ( ( ¬ ( 𝜑𝜓 ) ∧ 𝜓 ) → ¬ 𝜑 )