Theorem adantld

Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.)

Hypothesis
adantld.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \theta \wedge \psi \rightarrow \chi \)
Proof
l0
simpr
\( \vdash \theta \wedge \psi \rightarrow \psi \)
adantld.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syl5 l0 _