Metamath Proof Explorer

Theorem con2bii2

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

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

Proof

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