Theorem alcom 2160

Description: Theorem 19.5 of [Margaris] p. 89. Use its weak version alcomw 2044 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 1535

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  2337  sb8v  2358  sb8f  2359  sbnf2  2364  sbal1  2536  sbal2  2537  2mo2  2650  ralcom4  3292  ralcom4OLD  3293  ralcom  3295  nfra2wOLD  3306  ralcomf  3308  moelOLD  3413  sbccomlem  3891  unissbOLD  4964  dfiin2g  5055  dftr5OLD  5288  cotrgOLD  6140  cotrgOLDOLD  6141  cnvsymOLD  6145  cnvsymOLDOLD  6146  dffun2OLD  6584  dffun2OLDOLD  6585  fun11  6652  aceq1  10186  isch2  31255  dfon2lem8  35754  bj-hbaeb  36785  wl-sb9v  37503  wl-sbcom2d  37515  wl-sbalnae  37516  wl-2spsbbi  37519  cocossss  38392  cossssid3  38425  trcoss2  38440  dford4  42986  unielss  43179  elmapintrab  43538  undmrnresiss  43566  cnvssco  43568  elintima  43615  relexp0eq  43663  dfhe3  43737  dffrege115  43940  hbexg  44527  hbexgVD  44877  dfich2  47332  ichcom  47333