Theorem alcom 2199

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

Assertion

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

Proof of Theorem alcom

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-11 2197

This proof depends on definitions:  df-bi 210

This theorem is used by:  alrot3  2200  excom  2202  sbal  2209  sbcom2  2212  nfa2  2213  aaan  2366  sb8v  2385  sb8f  2386  sbnf2  2390  sbal1  2560  sbal2  2561  2mo2  2675  ralcom4  3292  ralcom  3294  ralcomf  3304  sbccomlem  3821  dfiin2g  4994  fun11  6644  aceq1  10235  isch2  31882  dfon2lem8  36767  bj-hbaeb  37946  bj-axseprep  38260  wl-sb9v  38749  wl-sbcom2d  38761  wl-sbalnae  38762  wl-2spsbbi  38765  cocossss  39724  cossssid3  39757  trcoss2  39772  dford4  44302  unielss  44481  elmapintrab  44838  undmrnresiss  44865  cnvssco  44867  elintima  44914  relexp0eq  44962  dfhe3  45036  dffrege115  45239  hbexg  45799  hbexgVD  46148  dfich2  48813  ichcom  48814