Metamath Proof Explorer

Theorem anass

Description: Associative law for conjunction. Theorem *4.32 of WhiteheadRussell p. 118. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 24-Nov-2012)

		Ref	Expression
	Assertion	anass	$⊢ ((φ \land ψ) \land χ) \leftrightarrow (φ \land (ψ \land χ))$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ (φ \land (ψ \land χ)) \to (φ \land (ψ \land χ))$
2	1	anassrs	$⊢ ((φ \land ψ) \land χ) \to (φ \land (ψ \land χ))$
3		id	$⊢ ((φ \land ψ) \land χ) \to ((φ \land ψ) \land χ)$
4	3	anasss	$⊢ (φ \land (ψ \land χ)) \to ((φ \land ψ) \land χ)$
5	2 4	impbii	$⊢ ((φ \land ψ) \land χ) \leftrightarrow (φ \land (ψ \land χ))$