# Metamath Proof Explorer

## Theorem andir

Description: Distributive law for conjunction. (Contributed by NM, 12-Aug-1994)

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

### Proof

Step Hyp Ref Expression
1 andi ${⊢}\left({\chi }\wedge \left({\phi }\vee {\psi }\right)\right)↔\left(\left({\chi }\wedge {\phi }\right)\vee \left({\chi }\wedge {\psi }\right)\right)$
2 ancom ${⊢}\left(\left({\phi }\vee {\psi }\right)\wedge {\chi }\right)↔\left({\chi }\wedge \left({\phi }\vee {\psi }\right)\right)$
3 ancom ${⊢}\left({\phi }\wedge {\chi }\right)↔\left({\chi }\wedge {\phi }\right)$
4 ancom ${⊢}\left({\psi }\wedge {\chi }\right)↔\left({\chi }\wedge {\psi }\right)$
5 3 4 orbi12i ${⊢}\left(\left({\phi }\wedge {\chi }\right)\vee \left({\psi }\wedge {\chi }\right)\right)↔\left(\left({\chi }\wedge {\phi }\right)\vee \left({\chi }\wedge {\psi }\right)\right)$
6 1 2 5 3bitr4i ${⊢}\left(\left({\phi }\vee {\psi }\right)\wedge {\chi }\right)↔\left(\left({\phi }\wedge {\chi }\right)\vee \left({\psi }\wedge {\chi }\right)\right)$