Theorem jcai

Deduction replacing implication with conjunction. (Contributed by NM, 15-Jul-1993.)

Hypotheses
jcai.1
\( \vdash \varphi \rightarrow \psi \)
jcai.2
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \wedge \chi \)
Proof
l0
jcai.1
l1
jcai.1
\( \vdash \varphi \rightarrow \psi \)
jcai.2
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
mpd l1 _
jca l0 _