Theorem ralrot3

Description: Rotate three restricted universal quantifiers. (Contributed by AV, 3-Dec-2021)

	Ref	Expression
Assertion	ralrot3	|- ( A. x e. A A. y e. B A. z e. C ph <-> A. z e. C A. x e. A A. y e. B ph )

Proof

Step	Hyp	Ref	Expression
1		ralcom	|- ( A. y e. B A. z e. C ph <-> A. z e. C A. y e. B ph )
2	1	ralbii	|- ( A. x e. A A. y e. B A. z e. C ph <-> A. x e. A A. z e. C A. y e. B ph )
3		ralcom	|- ( A. x e. A A. z e. C A. y e. B ph <-> A. z e. C A. x e. A A. y e. B ph )
4	2 3	bitri	|- ( A. x e. A A. y e. B A. z e. C ph <-> A. z e. C A. x e. A A. y e. B ph )