Theorem pm3.2i

Infer conjunction of premises. Inference associated with pm3.2. Its associated deduction is jca (and the double deduction is jcad ). (Contributed by NM, 21-Jun-1993.)

Hypotheses
pm3.2i.1
\( \vdash \varphi \)
pm3.2i.2
\( \vdash \psi \)
Conclusion
\( \vdash \varphi \wedge \psi \)
Proof
l0
pm3.2i.1
\( \vdash \varphi \)
l1
pm3.2i.2
\( \vdash \psi \)
pm3.2
\( \vdash \varphi \rightarrow \psi \rightarrow \varphi \wedge \psi \)
mp2 l0 l1 _