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 ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C φ ↔ ∀ z ∈ C ∀ y ∈ B ∀ x ∈ A φ

Proof

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