Metamath Proof Explorer

Theorem 3jaobOLD

Description: Obsolete version of 3jaob as of 29-Jun-2025. (Contributed by NM, 13-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

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