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