Theorem 3adantl1

Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)

Hypothesis
3adantl.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash (\tau \wedge \varphi \wedge \psi) \wedge \chi \rightarrow \theta \)
Proof
l0
3simpc
\( \vdash \tau \wedge \varphi \wedge \psi \rightarrow \varphi \wedge \psi \)
3adantl.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
sylan l0 _