Theorem jaoi

Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.)

Hypotheses
jaoi.1
\( \vdash \varphi \rightarrow \psi \)
jaoi.2
\( \vdash \chi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \vee \chi \rightarrow \psi \)
Proof
l0
pm2.53
\( \vdash \varphi \vee \chi \rightarrow \neg \varphi \rightarrow \chi \)
jaoi.2
\( \vdash \chi \rightarrow \psi \)
l2
syl6 l0 _
\( \vdash \varphi \vee \chi \rightarrow \neg \varphi \rightarrow \psi \)
jaoi.1
\( \vdash \varphi \rightarrow \psi \)
pm2.61d2 l2 _