Metamath Proof Explorer


Theorem 3jaoiOLD

Description: Obsolete version of 3jaoi as of 16-Jun-2026. Disjunction of three antecedents (inference). (Contributed by NM, 12-Sep-1995) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses 3jaoi.1 ⊢ φ → ψ
3jaoi.2 ⊢ χ → ψ
3jaoi.3 ⊢ θ → ψ
Assertion 3jaoiOLD ⊢ φ ∨ χ ∨ θ → ψ

Proof

Step Hyp Ref Expression
1 3jaoi.1 ⊢ φ → ψ
2 3jaoi.2 ⊢ χ → ψ
3 3jaoi.3 ⊢ θ → ψ
4 1 2 3 3pm3.2i ⊢ φ → ψ ∧ χ → ψ ∧ θ → ψ
5 3jao ⊢ φ → ψ ∧ χ → ψ ∧ θ → ψ → φ ∨ χ ∨ θ → ψ
6 4 5 ax-mp ⊢ φ ∨ χ ∨ θ → ψ