Theorem adantl

Inference adding a conjunct to the left of an antecedent. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)

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