Metamath Proof Explorer

Theorem pm5.18

Description: Theorem *5.18 of WhiteheadRussell p. 124. This theorem says that logical equivalence is the same as negated "exclusive or". (Contributed by NM, 28-Jun-2002) (Proof shortened by Andrew Salmon, 20-Jun-2011) (Proof shortened by Wolf Lammen, 15-Oct-2013)

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

Proof

Step Hyp Ref Expression
1 pm5.501 
 |-  ( ph -> ( -. ps <-> ( ph <-> -. ps ) ) )
2 1 con1bid 
 |-  ( ph -> ( -. ( ph <-> -. ps ) <-> ps ) )
3 pm5.501 
 |-  ( ph -> ( ps <-> ( ph <-> ps ) ) )
4 2 3 bitr2d 
 |-  ( ph -> ( ( ph <-> ps ) <-> -. ( ph <-> -. ps ) ) )
5 nbn2 
 |-  ( -. ph -> ( -. -. ps <-> ( ph <-> -. ps ) ) )
6 5 con1bid 
 |-  ( -. ph -> ( -. ( ph <-> -. ps ) <-> -. ps ) )
7 nbn2 
 |-  ( -. ph -> ( -. ps <-> ( ph <-> ps ) ) )
8 6 7 bitr2d 
 |-  ( -. ph -> ( ( ph <-> ps ) <-> -. ( ph <-> -. ps ) ) )
9 4 8 pm2.61i 
 |-  ( ( ph <-> ps ) <-> -. ( ph <-> -. ps ) )