Metamath Proof Explorer

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 
|- ( A. x e. A A. y e. B A. z e. C ph <-> A. z e. C A. y e. B A. x e. A ph )

Proof

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