Theorem adantl6r

Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)

Hypothesis
adantl6r.1
\( \vdash \varphi \wedge \eta \wedge \zeta \wedge \sigma \wedge \rho \wedge \mu \wedge \lambda \rightarrow \kappa \)
Conclusion
\( \vdash \varphi \wedge \tau \wedge \eta \wedge \zeta \wedge \sigma \wedge \rho \wedge \mu \wedge \lambda \rightarrow \kappa \)
Proof
adantl6r.1
ex _
adantl5r _
imp _