Theorem 3anassrs

Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)

Hypothesis
3anassrs.1
\( \vdash \varphi \wedge (\psi \wedge \chi \wedge \theta) \rightarrow \tau \)
Conclusion
\( \vdash \varphi \wedge \psi \wedge \chi \wedge \theta \rightarrow \tau \)
Proof
3anassrs.1
3exp2 _
imp41 _