Theorem 3adantr1

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 (\tau \wedge \psi \wedge \chi) \rightarrow \theta \)
Proof
l0
3simpc
\( \vdash \tau \wedge \psi \wedge \chi \rightarrow \psi \wedge \chi \)
3adantr.1
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \theta \)
sylan2 l0 _