Theorem alcom 2095

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

Assertion

Ref	Expression
alcom	⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)

Proof of Theorem alcom

Step	Hyp	Ref	Expression
1		ax-11 2093	. 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
2		ax-11 2093	. 2 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)
3	1, 2	impbii 201	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)

Syntax hints:   ↔ wb 198  ∀wal 1505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-11 2093

This theorem depends on definitions:  df-bi 199

This theorem is referenced by:  alrot3  2096  excom  2098  nfa2  2105  sbnf2  2291  sbcom2  2410  sbcom2OLD  2411  sbal1  2495  sbal2  2496  sbal2OLD  2497  sbal2OLDOLD  2498  sbal  2499  nexmoOLD  2549  2mo2  2679  ralcom4  3183  ralcom  3296  ralcomf  3299  unissb  4743  dfiin2g  4827  dftr5  5033  cotrg  5811  cnvsym  5814  dffun2  6198  fun11  6261  aceq1  9337  isch2  28779  moel  30034  dfon2lem8  32552  bj-hbaeb  33630  wl-sbcom2d  34235  wl-sbalnae  34236  wl-2spsbbi  34239  wl-dfralflem  34276  cocossss  35123  cossssid3  35151  trcoss2  35166  dford4  39019  elmapintrab  39295  undmrnresiss  39323  cnvssco  39325  elintima  39358  relexp0eq  39406  dfhe3  39481  dffrege115  39684  hbexg  40306  hbexgVD  40656  dfich2  42981  dfich2ai  42982  ichcom  42985