Theorem 3jaoi

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

Hypotheses
3jaoi.1
\( \vdash \varphi \rightarrow \psi \)
3jaoi.2
\( \vdash \chi \rightarrow \psi \)
3jaoi.3
\( \vdash \theta \rightarrow \psi \)
Conclusion
\( \vdash \varphi \vee \chi \vee \theta \rightarrow \psi \)
Proof
l0
3jaoi.1
\( \vdash \varphi \rightarrow \psi \)
l1
3jaoi.2
\( \vdash \chi \rightarrow \psi \)
l2
3jaoi.3
\( \vdash \theta \rightarrow \psi \)
3jaob
\( \vdash \varphi \vee \chi \vee \theta \rightarrow \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\chi \rightarrow \psi) \wedge (\theta \rightarrow \psi) \)
mpbir3an l0 l1 l2 _