Metamath Proof Explorer

Theorem notbi

Description: Contraposition. Theorem *4.11 of WhiteheadRussell p. 117. (Contributed by NM, 21-May-1994) (Proof shortened by Wolf Lammen, 12-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ( ph <-> ps ) -> ( ph <-> ps ) )
2 1 notbid 
 |-  ( ( ph <-> ps ) -> ( -. ph <-> -. ps ) )
3 id 
 |-  ( ( -. ph <-> -. ps ) -> ( -. ph <-> -. ps ) )
4 3 con4bid 
 |-  ( ( -. ph <-> -. ps ) -> ( ph <-> ps ) )
5 2 4 impbii 
 |-  ( ( ph <-> ps ) <-> ( -. ph <-> -. ps ) )