Theorem adantl3r

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

Hypothesis
adantl3r.1
\( \vdash \varphi \wedge \psi \wedge \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \wedge \eta \wedge \psi \wedge \chi \wedge \theta \rightarrow \tau \)
Proof
id
l1
adantlr _
\( \vdash \varphi \wedge \eta \wedge \psi \rightarrow \varphi \wedge \psi \)
adantl3r.1
\( \vdash \varphi \wedge \psi \wedge \chi \wedge \theta \rightarrow \tau \)
sylanl1 l1 _