Theorem not12an2impnot1 38784

Description: If a double conjunction is false and the second conjunct is true, then the first conjunct is false. http://us.metamath.org/other/completeusersproof/not12an2impnot1vd.html is the Virtual Deduction proof verified by automatically transforming it into the Metamath proof of not12an2impnot1 38784 using completeusersproof, which is verified by the Metamath program. http://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.)

Assertion

Ref	Expression
not12an2impnot1	|- ( ( -. ( ph /\ ps ) /\ ps ) -> -. ph )

Proof of Theorem not12an2impnot1

Step	Hyp	Ref	Expression
1		pm3.21 464	. . 3 |- ( ps -> ( ph -> ( ph /\ ps ) ) )
2	1	con3rr3 151	. 2 |- ( -. ( ph /\ ps ) -> ( ps -> -. ph ) )
3	2	imp 445	1 |- ( ( -. ( ph /\ ps ) /\ ps ) -> -. ph )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  sineq0ALT  39173