# Metamath Proof Explorer

## Theorem anddi

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

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

### Proof

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