# Metamath Proof Explorer

## Theorem andi

Description: Distributive law for conjunction. Theorem *4.4 of WhiteheadRussell p. 118. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 5-Jan-2013)

Ref Expression
Assertion andi ${⊢}\left({\phi }\wedge \left({\psi }\vee {\chi }\right)\right)↔\left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }\wedge {\chi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 orc ${⊢}\left({\phi }\wedge {\psi }\right)\to \left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }\wedge {\chi }\right)\right)$
2 olc ${⊢}\left({\phi }\wedge {\chi }\right)\to \left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }\wedge {\chi }\right)\right)$
3 1 2 jaodan ${⊢}\left({\phi }\wedge \left({\psi }\vee {\chi }\right)\right)\to \left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }\wedge {\chi }\right)\right)$
4 orc ${⊢}{\psi }\to \left({\psi }\vee {\chi }\right)$
5 4 anim2i ${⊢}\left({\phi }\wedge {\psi }\right)\to \left({\phi }\wedge \left({\psi }\vee {\chi }\right)\right)$
6 olc ${⊢}{\chi }\to \left({\psi }\vee {\chi }\right)$
7 6 anim2i ${⊢}\left({\phi }\wedge {\chi }\right)\to \left({\phi }\wedge \left({\psi }\vee {\chi }\right)\right)$
8 5 7 jaoi ${⊢}\left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }\wedge {\chi }\right)\right)\to \left({\phi }\wedge \left({\psi }\vee {\chi }\right)\right)$
9 3 8 impbii ${⊢}\left({\phi }\wedge \left({\psi }\vee {\chi }\right)\right)↔\left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }\wedge {\chi }\right)\right)$