Theorem alcom 2148

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

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 205  ∀wal 1531

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  alrot3  2149  excom  2151  sbal  2158  sbcom2  2162  nfa2  2165  aaan  2321  sb8v  2342  sb8f  2343  sbnf2  2348  sbal1  2521  sbal2  2522  2mo2  2635  ralcom4  3273  ralcom4OLD  3274  ralcom  3276  nfra2wOLD  3287  ralcomf  3289  moelOLD  3388  unissbOLD  4944  dfiin2g  5036  dftr5OLD  5271  cotrgOLD  6115  cotrgOLDOLD  6116  cnvsymOLD  6120  cnvsymOLDOLD  6121  dffun2OLD  6560  dffun2OLDOLD  6561  fun11  6628  aceq1  10142  isch2  31105  dfon2lem8  35517  bj-hbaeb  36427  wl-sb9v  37147  wl-sbcom2d  37159  wl-sbalnae  37160  wl-2spsbbi  37163  cocossss  38038  cossssid3  38071  trcoss2  38086  dford4  42592  unielss  42788  elmapintrab  43148  undmrnresiss  43176  cnvssco  43178  elintima  43225  relexp0eq  43273  dfhe3  43347  dffrege115  43550  hbexg  44137  hbexgVD  44487  dfich2  46935  ichcom  46936