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 | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑧 ∈ 𝐶 ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ralcom | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐶 𝜑 ) | |
| 2 | ralcom | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑧 ∈ 𝐶 ∀ 𝑥 ∈ 𝐴 𝜑 ) | |
| 3 | 2 | ralbii | ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 ∀ 𝑥 ∈ 𝐴 𝜑 ) |
| 4 | ralcom | ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑧 ∈ 𝐶 ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 ) | |
| 5 | 1 3 4 | 3bitri | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑧 ∈ 𝐶 ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 ) |