Theorem 3adantl2

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 (\varphi \wedge \tau \wedge \psi) \wedge \chi \rightarrow \theta \)
Proof
l0
3simpb
\( \vdash \varphi \wedge \tau \wedge \psi \rightarrow \varphi \wedge \psi \)
3adantl.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
sylan l0 _