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 φ