Theorem 3adantl3

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