Theorem adantrd

Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)

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