Metamath Proof Explorer

Theorem 3an4ancom24

Description: Commutative law for a conjunction with a triple conjunction: second and forth positions interchanged. (Contributed by AV, 18-Feb-2022)

		Ref	Expression
	Assertion	3an4ancom24	$⊢ ((φ \land ψ \land χ) \land θ) \leftrightarrow ((φ \land θ \land χ) \land ψ)$

Proof

Step	Hyp	Ref	Expression
1		an4com24	$⊢ ((φ \land ψ) \land (χ \land θ)) \leftrightarrow ((φ \land θ) \land (χ \land ψ))$
2		3an4anass	$⊢ ((φ \land ψ \land χ) \land θ) \leftrightarrow ((φ \land ψ) \land (χ \land θ))$
3		3an4anass	$⊢ ((φ \land θ \land χ) \land ψ) \leftrightarrow ((φ \land θ) \land (χ \land ψ))$
4	1 2 3	3bitr4i	$⊢ ((φ \land ψ \land χ) \land θ) \leftrightarrow ((φ \land θ \land χ) \land ψ)$