Theorem alcom 2165

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

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 206  ∀wal 1540

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  alrot3  2166  excom  2168  sbal  2175  sbcom2  2179  nfa2  2182  aaan  2338  sb8v  2358  sb8f  2359  sbnf2  2363  sbal1  2533  sbal2  2534  2mo2  2648  ralcom4  3264  ralcom  3266  ralcomf  3276  sbccomlem  3821  dfiin2g  4988  fun11  6574  aceq1  10039  isch2  31310  dfon2lem8  36001  bj-hbaeb  37064  bj-axseprep  37319  wl-sb9v  37801  wl-sbcom2d  37813  wl-sbalnae  37814  wl-2spsbbi  37817  cocossss  38774  cossssid3  38807  trcoss2  38822  dford4  43383  unielss  43572  elmapintrab  43929  undmrnresiss  43957  cnvssco  43959  elintima  44006  relexp0eq  44054  dfhe3  44128  dffrege115  44331  hbexg  44909  hbexgVD  45258  dfich2  47815  ichcom  47816