Theorem alcom 2161

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

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 206  ∀wal 1539

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  alrot3  2162  excom  2164  sbal  2171  sbcom2  2175  nfa2  2178  aaan  2332  sb8v  2352  sb8f  2353  sbnf2  2357  sbal1  2527  sbal2  2528  2mo2  2641  ralcom4  3256  ralcom  3258  ralcomf  3268  sbccomlem  3818  dfiin2g  4979  fun11  6551  aceq1  10000  isch2  31193  dfon2lem8  35803  bj-hbaeb  36832  wl-sb9v  37562  wl-sbcom2d  37574  wl-sbalnae  37575  wl-2spsbbi  37578  cocossss  38452  cossssid3  38485  trcoss2  38500  dford4  43041  unielss  43230  elmapintrab  43588  undmrnresiss  43616  cnvssco  43618  elintima  43665  relexp0eq  43713  dfhe3  43787  dffrege115  43990  hbexg  44568  hbexgVD  44917  dfich2  47468  ichcom  47469