Metamath Proof Explorer

Theorem orddi

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

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

Proof

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