Theorem jca

Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). Deduction form of pm3.2 and pm3.2i. Its associated deduction is jcad. Equivalent to the natural deduction rule /\ I ( /\ introduction), see [natded]. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

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