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