Theorem adantrlr

Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Hypothesis
adantr2.1
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge (\psi \wedge \tau \wedge \chi) \rightarrow \theta \)
Proof
l0
simpl
\( \vdash \psi \wedge \tau \rightarrow \psi \)
adantr2.1
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \theta \)
sylanr1 l0 _