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  2337  sb8v  2357  sb8f  2358  sbnf2  2362  sbal1  2532  sbal2  2533  2mo2  2647  ralcom4  3263  ralcom  3265  ralcomf  3275  sbccomlem  3807  dfiin2g  4973  fun11  6572  aceq1  10039  isch2  31294  dfon2lem8  35970  bj-hbaeb  37126  bj-axseprep  37381  wl-sb9v  37874  wl-sbcom2d  37886  wl-sbalnae  37887  wl-2spsbbi  37890  cocossss  38847  cossssid3  38880  trcoss2  38895  dford4  43457  unielss  43646  elmapintrab  44003  undmrnresiss  44031  cnvssco  44033  elintima  44080  relexp0eq  44128  dfhe3  44202  dffrege115  44405  hbexg  44983  hbexgVD  45332  dfich2  47918  ichcom  47919