Theorem alcom 2164

Description: Theorem 19.5 of [Margaris] p. 89. Use its weak version alcomw 2046 when it allows to avoid dependence on ax-11 2162. (Contributed by NM, 30-Jun-1993.)

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 206  ∀wal 1539

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  alrot3  2165  excom  2167  sbal  2174  sbcom2  2178  nfa2  2181  aaan  2337  sb8v  2357  sb8f  2358  sbnf2  2362  sbal1  2532  sbal2  2533  2mo2  2647  ralcom4  3262  ralcom  3264  ralcomf  3274  sbccomlem  3819  dfiin2g  4986  fun11  6566  aceq1  10027  isch2  31298  dfon2lem8  35982  bj-hbaeb  37020  wl-sb9v  37754  wl-sbcom2d  37766  wl-sbalnae  37767  wl-2spsbbi  37770  cocossss  38699  cossssid3  38732  trcoss2  38747  dford4  43271  unielss  43460  elmapintrab  43817  undmrnresiss  43845  cnvssco  43847  elintima  43894  relexp0eq  43942  dfhe3  44016  dffrege115  44219  hbexg  44797  hbexgVD  45146  dfich2  47704  ichcom  47705