Theorem
3adant3r1
Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)
Hypothesis
ad4ant3.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge (\tau \wedge \psi \wedge \chi) \rightarrow \theta \)
Proof
ad4ant3.1
3expb
_
3adantr1
_
This is the content in the right pane.