Theorem 3adantr2

Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)

Hypothesis
3adantr.1
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge (\psi \wedge \tau \wedge \chi) \rightarrow \theta \)
Proof
l0
3simpb
\( \vdash \psi \wedge \tau \wedge \chi \rightarrow \psi \wedge \chi \)
3adantr.1
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \theta \)
sylan2 l0 _