Theorem 3jaoiOLD

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.)

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
l1
3jaoi.2
3jaoi.3
l3
3pm3.2i l0 l1 _
\( \vdash (\varphi \rightarrow \psi) \wedge (\chi \rightarrow \psi) \wedge (\theta \rightarrow \psi) \)
3jao
\( \vdash (\varphi \rightarrow \psi) \wedge (\chi \rightarrow \psi) \wedge (\theta \rightarrow \psi) \rightarrow \varphi \vee \chi \vee \theta \rightarrow \psi \)
ax-mp l3 _