Metamath Proof Explorer

Theorem an4com24

Description: Rearrangement of 4 conjuncts: second and forth positions interchanged. (Contributed by AV, 18-Feb-2022)

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

Step	Hyp	Ref	Expression
1		an43	$⊢ ((φ \land ψ) \land (χ \land θ)) \leftrightarrow ((φ \land θ) \land (ψ \land χ))$
2		ancom	$⊢ (ψ \land χ) \leftrightarrow (χ \land ψ)$
3	2	anbi2i	$⊢ ((φ \land θ) \land (ψ \land χ)) \leftrightarrow ((φ \land θ) \land (χ \land ψ))$
4	1 3	bitri	$⊢ ((φ \land ψ) \land (χ \land θ)) \leftrightarrow ((φ \land θ) \land (χ \land ψ))$