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φ