4an21

Description: Rearrangement of 4 conjuncts with a triple conjunction. (Contributed by AV, 4-Mar-2022)

		Ref	Expression
	Assertion	4an21	$⊢ ((φ \land ψ) \land χ \land θ) \leftrightarrow (ψ \land (φ \land χ \land θ))$

Step	Hyp	Ref	Expression
1		3anass	$⊢ ((φ \land ψ) \land χ \land θ) \leftrightarrow ((φ \land ψ) \land (χ \land θ))$
2		ancom	$⊢ (φ \land ψ) \leftrightarrow (ψ \land φ)$
3	2	anbi1i	$⊢ ((φ \land ψ) \land (χ \land θ)) \leftrightarrow ((ψ \land φ) \land (χ \land θ))$
4		anass	$⊢ ((ψ \land φ) \land (χ \land θ)) \leftrightarrow (ψ \land (φ \land (χ \land θ)))$
5		3anass	$⊢ (φ \land χ \land θ) \leftrightarrow (φ \land (χ \land θ))$
6	5	bicomi	$⊢ (φ \land (χ \land θ)) \leftrightarrow (φ \land χ \land θ)$
7	6	anbi2i	$⊢ (ψ \land (φ \land (χ \land θ))) \leftrightarrow (ψ \land (φ \land χ \land θ))$
8	4 7	bitri	$⊢ ((ψ \land φ) \land (χ \land θ)) \leftrightarrow (ψ \land (φ \land χ \land θ))$
9	3 8	bitri	$⊢ ((φ \land ψ) \land (χ \land θ)) \leftrightarrow (ψ \land (φ \land χ \land θ))$
10	1 9	bitri	$⊢ ((φ \land ψ) \land χ \land θ) \leftrightarrow (ψ \land (φ \land χ \land θ))$

Metamath Proof Explorer