Metamath Proof Explorer

Theorem 3anasss

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

		Ref	Expression
	Hypothesis	3anasss.1	$⊢ (((φ \land ψ) \land χ) \land θ) \to τ$
	Assertion	3anasss	$⊢ (φ \land (ψ \land χ \land θ)) \to τ$

Proof

Step	Hyp	Ref	Expression
1		3anasss.1	$⊢ (((φ \land ψ) \land χ) \land θ) \to τ$
2		13an22anass	$⊢ (φ \land (ψ \land χ \land θ)) \leftrightarrow ((φ \land ψ) \land (χ \land θ))$
3	1	anasss	$⊢ ((φ \land ψ) \land (χ \land θ)) \to τ$
4	2 3	sylbi	$⊢ (φ \land (ψ \land χ \land θ)) \to τ$