Theorem ad5ant2345

Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.)

Hypothesis
ad5ant2345.1
\( \vdash \varphi \wedge \psi \wedge \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \eta \wedge \varphi \wedge \psi \wedge \chi \wedge \theta \rightarrow \tau \)
Proof
ad5ant2345.1
exp41 _
adantl _
imp41 _