# Metamath Proof Explorer

## Theorem or3dir

Description: Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017)

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

### Proof

Step Hyp Ref Expression
1 or3di ${⊢}\left({\tau }\vee \left({\phi }\wedge {\psi }\wedge {\chi }\right)\right)↔\left(\left({\tau }\vee {\phi }\right)\wedge \left({\tau }\vee {\psi }\right)\wedge \left({\tau }\vee {\chi }\right)\right)$
2 orcom ${⊢}\left({\tau }\vee \left({\phi }\wedge {\psi }\wedge {\chi }\right)\right)↔\left(\left({\phi }\wedge {\psi }\wedge {\chi }\right)\vee {\tau }\right)$
3 orcom ${⊢}\left({\tau }\vee {\phi }\right)↔\left({\phi }\vee {\tau }\right)$
4 orcom ${⊢}\left({\tau }\vee {\psi }\right)↔\left({\psi }\vee {\tau }\right)$
5 orcom ${⊢}\left({\tau }\vee {\chi }\right)↔\left({\chi }\vee {\tau }\right)$
6 3 4 5 3anbi123i ${⊢}\left(\left({\tau }\vee {\phi }\right)\wedge \left({\tau }\vee {\psi }\right)\wedge \left({\tau }\vee {\chi }\right)\right)↔\left(\left({\phi }\vee {\tau }\right)\wedge \left({\psi }\vee {\tau }\right)\wedge \left({\chi }\vee {\tau }\right)\right)$
7 1 2 6 3bitr3i ${⊢}\left(\left({\phi }\wedge {\psi }\wedge {\chi }\right)\vee {\tau }\right)↔\left(\left({\phi }\vee {\tau }\right)\wedge \left({\psi }\vee {\tau }\right)\wedge \left({\chi }\vee {\tau }\right)\right)$