**Description:** Theorem 19.5 of Margaris p. 89. (Contributed by NM, 30-Jun-1993)

Ref | Expression | ||
---|---|---|---|

Assertion | alcom | ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 𝜑 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | ax-11 | ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 ) | |

2 | ax-11 | ⊢ ( ∀ 𝑦 ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜑 ) | |

3 | 1 2 | impbii | ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 𝜑 ) |