Theorem ad7antlr

Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)

Hypothesis
ad2ant.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \chi \wedge \varphi \wedge \theta \wedge \tau \wedge \eta \wedge \zeta \wedge \sigma \wedge \rho \rightarrow \psi \)
Proof
ad2ant.1
adantl _
ad6antr _