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  3808  dfiin2g  4974  fun11  6566  aceq1  10030  isch2  31309  dfon2lem8  35986  bj-hbaeb  37142  bj-axseprep  37397  wl-sb9v  37888  wl-sbcom2d  37900  wl-sbalnae  37901  wl-2spsbbi  37904  cocossss  38861  cossssid3  38894  trcoss2  38909  dford4  43475  unielss  43664  elmapintrab  44021  undmrnresiss  44049  cnvssco  44051  elintima  44098  relexp0eq  44146  dfhe3  44220  dffrege115  44423  hbexg  45001  hbexgVD  45350  dfich2  47930  ichcom  47931