Theorem alcom 2160

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

Assertion

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

Proof of Theorem alcom

Step	Hyp	Ref	Expression
1		ax-11 2158	. 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
2		ax-11 2158	. 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 2158

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  alrot3  2161  excom  2163  sbal  2170  sbcom2  2174  nfa2  2177  aaan  2331  sb8v  2351  sb8f  2352  sbnf2  2357  sbal1  2527  sbal2  2528  2mo2  2641  ralcom4  3264  ralcom  3266  ralcomf  3278  sbccomlem  3835  unissbOLD  4907  dfiin2g  4999  dftr5OLD  5222  cotrgOLD  6084  cotrgOLDOLD  6085  cnvsymOLD  6089  cnvsymOLDOLD  6090  dffun2OLD  6525  dffun2OLDOLD  6526  fun11  6593  aceq1  10077  isch2  31159  dfon2lem8  35785  bj-hbaeb  36814  wl-sb9v  37544  wl-sbcom2d  37556  wl-sbalnae  37557  wl-2spsbbi  37560  cocossss  38434  cossssid3  38467  trcoss2  38482  dford4  43025  unielss  43214  elmapintrab  43572  undmrnresiss  43600  cnvssco  43602  elintima  43649  relexp0eq  43697  dfhe3  43771  dffrege115  43974  hbexg  44553  hbexgVD  44902  dfich2  47463  ichcom  47464