Theorem 3adantr3

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