Theorem alcom 2156

Description: Theorem 19.5 of [Margaris] p. 89. Use its weak version alcomw 2047 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 208	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)

Syntax hints:   ↔ wb 205  ∀wal 1539

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 206

This theorem is referenced by:  alrot3  2157  sbal  2159  sbcom2  2161  excom  2162  nfa2  2170  aaan  2327  sb8v  2348  sb8f  2349  sbnf2  2354  sbal1  2526  sbal2  2527  2mo2  2642  ralcom4  3267  ralcom4OLD  3268  ralcom  3270  nfra2wOLD  3281  ralcomf  3283  moelOLD  3376  unissbOLD  4906  dfiin2g  4997  dftr5OLD  5232  cotrgOLD  6067  cotrgOLDOLD  6068  cnvsymOLD  6072  cnvsymOLDOLD  6073  dffun2OLD  6512  dffun2OLDOLD  6513  fun11  6580  aceq1  10062  isch2  30228  dfon2lem8  34451  bj-hbaeb  35360  wl-sbcom2d  36089  wl-sbalnae  36090  wl-2spsbbi  36093  cocossss  36971  cossssid3  37004  trcoss2  37019  dford4  41411  unielss  41610  elmapintrab  41970  undmrnresiss  41998  cnvssco  42000  elintima  42047  relexp0eq  42095  dfhe3  42169  dffrege115  42372  hbexg  42960  hbexgVD  43310  dfich2  45770  ichcom  45771