Theorem 3pm3.2i

Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)

Hypotheses
3pm3.2i.1
\( \vdash \varphi \)
3pm3.2i.2
\( \vdash \psi \)
3pm3.2i.3
\( \vdash \chi \)
Conclusion
\( \vdash \varphi \wedge \psi \wedge \chi \)
Proof
l0
3pm3.2i.1
3pm3.2i.2
l2
pm3.2i l0 _
\( \vdash \varphi \wedge \psi \)
l3
3pm3.2i.3
\( \vdash \chi \)
df-3an
\( \vdash \varphi \wedge \psi \wedge \chi \leftrightarrow \varphi \wedge \psi \wedge \chi \)
mpbir2an l2 l3 _