Metamath Proof Explorer


Theorem con3ALT2

Description: Contraposition. Alternate proof of con3 . This proof is con3ALTVD automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion con3ALT2
|- ( ( ph -> ps ) -> ( -. ps -> -. ph ) )

Proof

Step Hyp Ref Expression
1 notnotr
 |-  ( -. -. ph -> ph )
2 1 imim1i
 |-  ( ( ph -> ps ) -> ( -. -. ph -> ps ) )
3 2 con1d
 |-  ( ( ph -> ps ) -> ( -. ps -> -. ph ) )