Theorem
3ad2antr1
Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)
Hypothesis
3ad2antl.1
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge (\chi \wedge \psi \wedge \tau) \rightarrow \theta \)
Proof
3ad2antl.1
adantrr
_
3adantr3
_
This is the content in the right pane.