# 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 ${⊢}\left({\phi }↔{\psi }\right)↔¬\left({\phi }↔¬{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 pm5.501 ${⊢}{\phi }\to \left(¬{\psi }↔\left({\phi }↔¬{\psi }\right)\right)$
2 1 con1bid ${⊢}{\phi }\to \left(¬\left({\phi }↔¬{\psi }\right)↔{\psi }\right)$
3 pm5.501 ${⊢}{\phi }\to \left({\psi }↔\left({\phi }↔{\psi }\right)\right)$
4 2 3 bitr2d ${⊢}{\phi }\to \left(\left({\phi }↔{\psi }\right)↔¬\left({\phi }↔¬{\psi }\right)\right)$
5 nbn2 ${⊢}¬{\phi }\to \left(¬¬{\psi }↔\left({\phi }↔¬{\psi }\right)\right)$
6 5 con1bid ${⊢}¬{\phi }\to \left(¬\left({\phi }↔¬{\psi }\right)↔¬{\psi }\right)$
7 nbn2 ${⊢}¬{\phi }\to \left(¬{\psi }↔\left({\phi }↔{\psi }\right)\right)$
8 6 7 bitr2d ${⊢}¬{\phi }\to \left(\left({\phi }↔{\psi }\right)↔¬\left({\phi }↔¬{\psi }\right)\right)$
9 4 8 pm2.61i ${⊢}\left({\phi }↔{\psi }\right)↔¬\left({\phi }↔¬{\psi }\right)$