Metamath Proof Explorer

Theorem ralrot3

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

Ref Expression
Assertion ralrot3 ⊢∀x∈A∀y∈B∀z∈Cφ↔∀z∈C∀x∈A∀y∈Bφ

Proof

Step Hyp Ref Expression
1 ralcom ⊢∀y∈B∀z∈Cφ↔∀z∈C∀y∈Bφ
2 1 ralbii ⊢∀x∈A∀y∈B∀z∈Cφ↔∀x∈A∀z∈C∀y∈Bφ
3 ralcom ⊢∀x∈A∀z∈C∀y∈Bφ↔∀z∈C∀x∈A∀y∈Bφ
4 2 3 bitri ⊢∀x∈A∀y∈B∀z∈Cφ↔∀z∈C∀x∈A∀y∈Bφ