Theorem alcom 2157

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

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 205  ∀wal 1540

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  alrot3  2158  sbal  2160  sbcom2  2162  excom  2163  nfa2  2171  aaan  2328  sb8v  2349  sb8f  2350  sbnf2  2355  sbal1  2528  sbal2  2529  2mo2  2644  ralcom4  3284  ralcom4OLD  3285  ralcom  3287  nfra2wOLD  3298  ralcomf  3300  moelOLD  3402  unissbOLD  4945  dfiin2g  5036  dftr5OLD  5271  cotrgOLD  6110  cotrgOLDOLD  6111  cnvsymOLD  6115  cnvsymOLDOLD  6116  dffun2OLD  6555  dffun2OLDOLD  6556  fun11  6623  aceq1  10112  isch2  30476  dfon2lem8  34762  bj-hbaeb  35697  wl-sbcom2d  36426  wl-sbalnae  36427  wl-2spsbbi  36430  cocossss  37306  cossssid3  37339  trcoss2  37354  dford4  41768  unielss  41967  elmapintrab  42327  undmrnresiss  42355  cnvssco  42357  elintima  42404  relexp0eq  42452  dfhe3  42526  dffrege115  42729  hbexg  43317  hbexgVD  43667  dfich2  46126  ichcom  46127