# Metamath Proof Explorer

## Theorem pm5.32

Description: Distribution of implication over biconditional. Theorem *5.32 of WhiteheadRussell p. 125. (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion pm5.32 ${⊢}\left({\phi }\to \left({\psi }↔{\chi }\right)\right)↔\left(\left({\phi }\wedge {\psi }\right)↔\left({\phi }\wedge {\chi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 notbi ${⊢}\left({\psi }↔{\chi }\right)↔\left(¬{\psi }↔¬{\chi }\right)$
2 1 imbi2i ${⊢}\left({\phi }\to \left({\psi }↔{\chi }\right)\right)↔\left({\phi }\to \left(¬{\psi }↔¬{\chi }\right)\right)$
3 pm5.74 ${⊢}\left({\phi }\to \left(¬{\psi }↔¬{\chi }\right)\right)↔\left(\left({\phi }\to ¬{\psi }\right)↔\left({\phi }\to ¬{\chi }\right)\right)$
4 notbi ${⊢}\left(\left({\phi }\to ¬{\psi }\right)↔\left({\phi }\to ¬{\chi }\right)\right)↔\left(¬\left({\phi }\to ¬{\psi }\right)↔¬\left({\phi }\to ¬{\chi }\right)\right)$
5 2 3 4 3bitri ${⊢}\left({\phi }\to \left({\psi }↔{\chi }\right)\right)↔\left(¬\left({\phi }\to ¬{\psi }\right)↔¬\left({\phi }\to ¬{\chi }\right)\right)$
6 df-an ${⊢}\left({\phi }\wedge {\psi }\right)↔¬\left({\phi }\to ¬{\psi }\right)$
7 df-an ${⊢}\left({\phi }\wedge {\chi }\right)↔¬\left({\phi }\to ¬{\chi }\right)$
8 6 7 bibi12i ${⊢}\left(\left({\phi }\wedge {\psi }\right)↔\left({\phi }\wedge {\chi }\right)\right)↔\left(¬\left({\phi }\to ¬{\psi }\right)↔¬\left({\phi }\to ¬{\chi }\right)\right)$
9 5 8 bitr4i ${⊢}\left({\phi }\to \left({\psi }↔{\chi }\right)\right)↔\left(\left({\phi }\wedge {\psi }\right)↔\left({\phi }\wedge {\chi }\right)\right)$