Theorem alcom 2200

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

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 209  ∀wal 1565

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

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  alrot3  2201  excom  2203  sbal  2210  sbcom2  2213  nfa2  2216  aaan  2371  sb8v  2391  sb8f  2392  sbnf2  2396  sbal1  2566  sbal2  2567  2mo2  2681  ralcom4  3297  ralcom  3299  ralcomf  3309  sbccomlem  3831  dfiin2g  4996  fun11  6607  aceq1  10097  isch2  31512  dfon2lem8  36175  bj-hbaeb  37339  bj-axseprep  37594  wl-sb9v  38087  wl-sbcom2d  38099  wl-sbalnae  38100  wl-2spsbbi  38103  cocossss  39060  cossssid3  39093  trcoss2  39108  dford4  43641  unielss  43830  elmapintrab  44187  undmrnresiss  44215  cnvssco  44217  elintima  44264  relexp0eq  44312  dfhe3  44386  dffrege115  44589  hbexg  45150  hbexgVD  45499  dfich2  48089  ichcom  48090