Theorem alcom 2156

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

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 206  ∀wal 1534

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  alrot3  2157  excom  2159  sbal  2166  sbcom2  2170  nfa2  2173  aaan  2331  sb8v  2352  sb8f  2353  sbnf2  2358  sbal1  2530  sbal2  2531  2mo2  2644  ralcom4  3283  ralcom4OLD  3284  ralcom  3286  nfra2wOLD  3297  ralcomf  3299  moelOLD  3402  sbccomlem  3877  unissbOLD  4944  dfiin2g  5036  dftr5OLD  5269  cotrgOLD  6130  cotrgOLDOLD  6131  cnvsymOLD  6135  cnvsymOLDOLD  6136  dffun2OLD  6573  dffun2OLDOLD  6574  fun11  6641  aceq1  10154  isch2  31251  dfon2lem8  35771  bj-hbaeb  36801  wl-sb9v  37529  wl-sbcom2d  37541  wl-sbalnae  37542  wl-2spsbbi  37545  cocossss  38417  cossssid3  38450  trcoss2  38465  dford4  43017  unielss  43206  elmapintrab  43565  undmrnresiss  43593  cnvssco  43595  elintima  43642  relexp0eq  43690  dfhe3  43764  dffrege115  43967  hbexg  44553  hbexgVD  44903  dfich2  47382  ichcom  47383