Theorem pm3.2

Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. Its associated inference is pm3.2i and its associated deduction is jca (and the double deduction is jcad ). See pm3.2im for a version using only implication and negation. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)

Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \varphi \wedge \psi \)
Proof
id
ex _