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  2335  sb8v  2355  sb8f  2356  sbnf2  2360  sbal1  2530  sbal2  2531  2mo2  2644  ralcom4  3259  ralcom  3261  ralcomf  3271  sbccomlem  3816  dfiin2g  4983  fun11  6563  aceq1  10019  isch2  31224  dfon2lem8  35904  bj-hbaeb  36936  wl-sb9v  37666  wl-sbcom2d  37678  wl-sbalnae  37679  wl-2spsbbi  37682  cocossss  38611  cossssid3  38644  trcoss2  38659  dford4  43186  unielss  43375  elmapintrab  43733  undmrnresiss  43761  cnvssco  43763  elintima  43810  relexp0eq  43858  dfhe3  43932  dffrege115  44135  hbexg  44713  hbexgVD  45062  dfich2  47620  ichcom  47621