Theorem
ad2ant2r
Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
ad2ant2.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \theta \wedge (\psi \wedge \tau) \rightarrow \chi \)
Proof
ad2ant2.1
adantrr
_
adantlr
_
This is the content in the right pane.