Metamath Proof Explorer

Theorem or3di

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

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

Proof

Step Hyp Ref Expression
1 df-3an ⊢ ψ ∧ χ ∧ τ ↔ ψ ∧ χ ∧ τ
2 1 orbi2i ⊢ φ ∨ ψ ∧ χ ∧ τ ↔ φ ∨ ψ ∧ χ ∧ τ
3 ordi ⊢ φ ∨ ψ ∧ χ ∧ τ ↔ φ ∨ ψ ∧ χ ∧ φ ∨ τ
4 ordi ⊢ φ ∨ ψ ∧ χ ↔ φ ∨ ψ ∧ φ ∨ χ
5 4 anbi1i ⊢ φ ∨ ψ ∧ χ ∧ φ ∨ τ ↔ φ ∨ ψ ∧ φ ∨ χ ∧ φ ∨ τ
6 2 3 5 3bitri ⊢ φ ∨ ψ ∧ χ ∧ τ ↔ φ ∨ ψ ∧ φ ∨ χ ∧ φ ∨ τ
7 df-3an ⊢ φ ∨ ψ ∧ φ ∨ χ ∧ φ ∨ τ ↔ φ ∨ ψ ∧ φ ∨ χ ∧ φ ∨ τ
8 6 7 bitr4i ⊢ φ ∨ ψ ∧ χ ∧ τ ↔ φ ∨ ψ ∧ φ ∨ χ ∧ φ ∨ τ