Metamath Proof Explorer

Theorem or3dir

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

Ref Expression
Assertion or3dir ⊢ φ ∧ ψ ∧ χ ∨ τ ↔ φ ∨ τ ∧ ψ ∨ τ ∧ χ ∨ τ

Proof

Step Hyp Ref Expression
1 or3di ⊢ τ ∨ φ ∧ ψ ∧ χ ↔ τ ∨ φ ∧ τ ∨ ψ ∧ τ ∨ χ
2 orcom ⊢ τ ∨ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ ∨ τ
3 orcom ⊢ τ ∨ φ ↔ φ ∨ τ
4 orcom ⊢ τ ∨ ψ ↔ ψ ∨ τ
5 orcom ⊢ τ ∨ χ ↔ χ ∨ τ
6 3 4 5 3anbi123i ⊢ τ ∨ φ ∧ τ ∨ ψ ∧ τ ∨ χ ↔ φ ∨ τ ∧ ψ ∨ τ ∧ χ ∨ τ
7 1 2 6 3bitr3i ⊢ φ ∧ ψ ∧ χ ∨ τ ↔ φ ∨ τ ∧ ψ ∨ τ ∧ χ ∨ τ