Metamath Proof Explorer


Theorem 3jaoi

Description: Disjunction of three antecedents (inference). (Contributed by NM, 12-Sep-1995) (Proof shortened by Garrett Katz, 16-Jun-2026)

Ref Expression
Hypotheses 3jaoi.1 φ ψ
3jaoi.2 χ ψ
3jaoi.3 θ ψ
Assertion 3jaoi φ χ θ ψ

Proof

Step Hyp Ref Expression
1 3jaoi.1 φ ψ
2 3jaoi.2 χ ψ
3 3jaoi.3 θ ψ
4 3jaob φ χ θ ψ φ ψ χ ψ θ ψ
5 1 2 3 4 mpbir3an φ χ θ ψ