Theorem jcad

Deduction conjoining the consequents of two implications. Deduction form of jca and double deduction form of pm3.2 and pm3.2i. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)

Hypotheses
jcad.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
jcad.2
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \wedge \theta \)
Proof
l0
jcad.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
l1
jcad.2
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
pm3.2
\( \vdash \chi \rightarrow \theta \rightarrow \chi \wedge \theta \)
syl6c l0 l1 _