Metamath Proof Explorer

Theorem andi3or

Description: Distribute over triple disjunction. (Contributed by RP, 5-Jul-2021)

Ref Expression
Assertion andi3or ⊢ φ ∧ ψ ∨ χ ∨ θ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ φ ∧ θ

Proof

Step Hyp Ref Expression
1 andi ⊢ φ ∧ ψ ∨ χ ∨ θ ↔ φ ∧ ψ ∨ χ ∨ φ ∧ θ
2 andi ⊢ φ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ φ ∧ χ
3 2 orbi1i ⊢ φ ∧ ψ ∨ χ ∨ φ ∧ θ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ φ ∧ θ
4 1 3 bitri ⊢ φ ∧ ψ ∨ χ ∨ θ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ φ ∧ θ
5 df-3or ⊢ ψ ∨ χ ∨ θ ↔ ψ ∨ χ ∨ θ
6 5 anbi2i ⊢ φ ∧ ψ ∨ χ ∨ θ ↔ φ ∧ ψ ∨ χ ∨ θ
7 df-3or ⊢ φ ∧ ψ ∨ φ ∧ χ ∨ φ ∧ θ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ φ ∧ θ
8 4 6 7 3bitr4i ⊢ φ ∧ ψ ∨ χ ∨ θ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ φ ∧ θ