Theorem 3anasss

Associative law for conjunction applied to antecedent (eliminates syllogism). Converse of 3anassrs. (Contributed by Thierry Arnoux, 5-Jul-2026.)

Hypothesis
3anasss.1
\( \vdash \varphi \wedge \psi \wedge \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \wedge (\psi \wedge \chi \wedge \theta) \rightarrow \tau \)
Proof
l0
13an22anass
\( \vdash \varphi \wedge (\psi \wedge \chi \wedge \theta) \leftrightarrow \varphi \wedge \psi \wedge (\chi \wedge \theta) \)
3anasss.1
anasss _
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \rightarrow \tau \)
sylbi l0 _