Metamath Proof Explorer

Theorem 3jaob

Description: Disjunction of three antecedents. (Contributed by NM, 13-Sep-2011)

Ref Expression
Assertion 3jaob ⊢ φ ∨ χ ∨ θ → ψ ↔ φ → ψ ∧ χ → ψ ∧ θ → ψ

Proof

Step Hyp Ref Expression
1 3mix1 ⊢ φ → φ ∨ χ ∨ θ
2 1 imim1i ⊢ φ ∨ χ ∨ θ → ψ → φ → ψ
3 3mix2 ⊢ χ → φ ∨ χ ∨ θ
4 3 imim1i ⊢ φ ∨ χ ∨ θ → ψ → χ → ψ
5 3mix3 ⊢ θ → φ ∨ χ ∨ θ
6 5 imim1i ⊢ φ ∨ χ ∨ θ → ψ → θ → ψ
7 2 4 6 3jca ⊢ φ ∨ χ ∨ θ → ψ → φ → ψ ∧ χ → ψ ∧ θ → ψ
8 3jao ⊢ φ → ψ ∧ χ → ψ ∧ θ → ψ → φ ∨ χ ∨ θ → ψ
9 7 8 impbii ⊢ φ ∨ χ ∨ θ → ψ ↔ φ → ψ ∧ χ → ψ ∧ θ → ψ