Theorem alcom 2159

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

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 206  ∀wal 1538

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  alrot3  2160  excom  2162  sbal  2169  sbcom2  2173  nfa2  2176  aaan  2333  sb8v  2355  sb8f  2356  sbnf2  2361  sbal1  2533  sbal2  2534  2mo2  2647  ralcom4  3286  ralcom4OLD  3287  ralcom  3289  nfra2wOLD  3300  ralcomf  3302  moelOLD  3405  sbccomlem  3869  unissbOLD  4940  dfiin2g  5032  dftr5OLD  5264  cotrgOLD  6128  cotrgOLDOLD  6129  cnvsymOLD  6133  cnvsymOLDOLD  6134  dffun2OLD  6572  dffun2OLDOLD  6573  fun11  6640  aceq1  10157  isch2  31242  dfon2lem8  35791  bj-hbaeb  36820  wl-sb9v  37550  wl-sbcom2d  37562  wl-sbalnae  37563  wl-2spsbbi  37566  cocossss  38437  cossssid3  38470  trcoss2  38485  dford4  43041  unielss  43230  elmapintrab  43589  undmrnresiss  43617  cnvssco  43619  elintima  43666  relexp0eq  43714  dfhe3  43788  dffrege115  43991  hbexg  44576  hbexgVD  44926  dfich2  47445  ichcom  47446