Theorem ralcom13

Description: Swap first and third restricted universal quantifiers. (Contributed by AV, 3-Dec-2021) (Proof shortened by Wolf Lammen, 2-Jan-2025)

	Ref	Expression
Assertion	ralcom13	$$⊢\forall x\in A\forall y\in B\forall z\in C\phi \leftrightarrow \forall z\in C\forall y\in B\forall x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		ralrot3	$$⊢\forall x\in A\forall y\in B\forall z\in C\phi \leftrightarrow \forall z\in C\forall x\in A\forall y\in B\phi$$
2		ralcom	$$⊢\forall x\in A\forall y\in B\phi \leftrightarrow \forall y\in B\forall x\in A\phi$$
3	2	ralbii	$$⊢\forall z\in C\forall x\in A\forall y\in B\phi \leftrightarrow \forall z\in C\forall y\in B\forall x\in A\phi$$
4	1 3	bitri	$$⊢\forall x\in A\forall y\in B\forall z\in C\phi \leftrightarrow \forall z\in C\forall y\in B\forall x\in A\phi$$