Theorem 3jca

Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)

Hypotheses
3jca.1
\( \vdash \varphi \rightarrow \psi \)
3jca.2
\( \vdash \varphi \rightarrow \chi \)
3jca.3
\( \vdash \varphi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \wedge \chi \wedge \theta \)
Proof
l0
3jca.1
l1
3jca.2
3jca.3
l3
jca31 l0 l1 _
\( \vdash \varphi \rightarrow \psi \wedge \chi \wedge \theta \)
df-3an
\( \vdash \psi \wedge \chi \wedge \theta \leftrightarrow \psi \wedge \chi \wedge \theta \)
sylibr l3 _