Metamath Proof Explorer

Theorem ralcom13OLD

Description: Obsolete version of ralcom13 as of 2-Jan-2025. (Contributed by AV, 3-Dec-2021) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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