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 φ ψ ¬ ψ ¬ φ

Proof

Step Hyp Ref Expression
1 notnotr ¬ ¬ φ φ
2 1 imim1i φ ψ ¬ ¬ φ ψ
3 2 con1d φ ψ ¬ ψ ¬ φ