Metamath Proof Explorer

Theorem con34b

Description: A biconditional form of contraposition. Theorem *4.1 of WhiteheadRussell p. 116. (Contributed by NM, 11-May-1993)

Ref Expression
Assertion con34b 
|- ( ( ph -> ps ) <-> ( -. ps -> -. ph ) )

Proof

Step Hyp Ref Expression
1 con3 
 |-  ( ( ph -> ps ) -> ( -. ps -> -. ph ) )
2 con4 
 |-  ( ( -. ps -> -. ph ) -> ( ph -> ps ) )
3 1 2 impbii 
 |-  ( ( ph -> ps ) <-> ( -. ps -> -. ph ) )