Theorem adantl4r

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

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