Theorem ja

Inference joining the antecedents of two premises. For partial converses, see jarri and jarli. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.)

Hypotheses
ja.1
\( \vdash \neg \varphi \rightarrow \chi \)
ja.2
\( \vdash \psi \rightarrow \chi \)
Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow \chi \)
Proof
ja.2
l1
imim2i _
\( \vdash (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
ja.1
\( \vdash \neg \varphi \rightarrow \chi \)
pm2.61d1 l1 _