Theorem adantr

Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.)

Hypothesis
adantr.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \wedge \chi \rightarrow \psi \)
Proof
adantr.1
a1d _
imp _