Theorem alcom 2170

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

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 207  ∀wal 1545

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

This theorem depends on definitions:  df-bi 208

This theorem is referenced by:  alrot3  2171  excom  2173  sbal  2180  sbcom2  2183  nfa2  2186  aaan  2341  sb8v  2361  sb8f  2362  sbnf2  2366  sbal1  2536  sbal2  2537  2mo2  2651  ralcom4  3265  ralcom  3267  ralcomf  3277  sbccomlem  3801  dfiin2g  4960  fun11  6559  aceq1  10030  isch2  31312  dfon2lem8  36016  bj-hbaeb  37172  bj-axseprep  37427  wl-sb9v  37920  wl-sbcom2d  37932  wl-sbalnae  37933  wl-2spsbbi  37936  cocossss  38893  cossssid3  38926  trcoss2  38941  dford4  43474  unielss  43663  elmapintrab  44020  undmrnresiss  44048  cnvssco  44050  elintima  44097  relexp0eq  44145  dfhe3  44219  dffrege115  44422  hbexg  45000  hbexgVD  45349  dfich2  47933  ichcom  47934