Theorem
ad2antll
Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
Hypothesis
ad2ant.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \chi \wedge (\theta \wedge \varphi) \rightarrow \psi \)
Proof
ad2ant.1
adantl
_
adantl
_
This is the content in the right pane.