Metamath Proof Explorer


Theorem con1bii

Description: A contraposition inference. (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 13-Oct-2012)

Ref Expression
Hypothesis con1bii.1 ¬φψ
Assertion con1bii ¬ψφ

Proof

Step Hyp Ref Expression
1 con1bii.1 ¬φψ
2 notnotb φ¬¬φ
3 2 1 xchbinx φ¬ψ
4 3 bicomi ¬ψφ