# Metamath Proof Explorer

## Theorem pm5.17

Description: Theorem *5.17 of WhiteheadRussell p. 124. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 3-Jan-2013)

Ref Expression
Assertion pm5.17 ${⊢}\left(\left({\phi }\vee {\psi }\right)\wedge ¬\left({\phi }\wedge {\psi }\right)\right)↔\left({\phi }↔¬{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 bicom ${⊢}\left({\phi }↔¬{\psi }\right)↔\left(¬{\psi }↔{\phi }\right)$
2 dfbi2 ${⊢}\left(¬{\psi }↔{\phi }\right)↔\left(\left(¬{\psi }\to {\phi }\right)\wedge \left({\phi }\to ¬{\psi }\right)\right)$
3 orcom ${⊢}\left({\phi }\vee {\psi }\right)↔\left({\psi }\vee {\phi }\right)$
4 df-or ${⊢}\left({\psi }\vee {\phi }\right)↔\left(¬{\psi }\to {\phi }\right)$
5 3 4 bitr2i ${⊢}\left(¬{\psi }\to {\phi }\right)↔\left({\phi }\vee {\psi }\right)$
6 imnan ${⊢}\left({\phi }\to ¬{\psi }\right)↔¬\left({\phi }\wedge {\psi }\right)$
7 5 6 anbi12i ${⊢}\left(\left(¬{\psi }\to {\phi }\right)\wedge \left({\phi }\to ¬{\psi }\right)\right)↔\left(\left({\phi }\vee {\psi }\right)\wedge ¬\left({\phi }\wedge {\psi }\right)\right)$
8 1 2 7 3bitrri ${⊢}\left(\left({\phi }\vee {\psi }\right)\wedge ¬\left({\phi }\wedge {\psi }\right)\right)↔\left({\phi }↔¬{\psi }\right)$