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 ⊢φ∨ψ∧χ∧τ↔φ∨ψ∧φ∨χ∧φ∨τ