Metamath Proof Explorer

Theorem con1bii2

Description: A contraposition inference. (Contributed by ML, 18-Oct-2020)

Ref Expression
Hypothesis con1bii2.1 
|- ( -. ph <-> ps )
Assertion con1bii2 
|- ( ph <-> -. ps )

Proof

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