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 
|- ( -. ph <-> ps )
Assertion con1bii 
|- ( -. ps <-> ph )

Proof

Step Hyp Ref Expression
1 con1bii.1 
 |-  ( -. ph <-> ps )
2 notnotb 
 |-  ( ph <-> -. -. ph )
3 2 1 xchbinx 
 |-  ( ph <-> -. ps )
4 3 bicomi 
 |-  ( -. ps <-> ph )