Theorem adantl5r

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

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