Theorem alcom 2197

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

Assertion

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

Proof of Theorem alcom

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-11 2195

This proof depends on definitions:  df-bi 210

This theorem is used by:  alrot3  2198  excom  2200  sbal  2207  sbcom2  2210  nfa2  2213  aaan  2367  sb8v  2387  sb8f  2388  sbnf2  2392  sbal1  2562  sbal2  2563  2mo2  2677  ralcom4  3293  ralcom  3295  ralcomf  3305  sbccomlem  3824  dfiin2g  4997  fun11  6614  aceq1  10113  isch2  31604  dfon2lem8  36293  bj-hbaeb  37487  bj-axseprep  37744  wl-sb9v  38237  wl-sbcom2d  38249  wl-sbalnae  38250  wl-2spsbbi  38253  cocossss  39208  cossssid3  39241  trcoss2  39256  dford4  43789  unielss  43978  elmapintrab  44335  undmrnresiss  44363  cnvssco  44365  elintima  44412  relexp0eq  44460  dfhe3  44534  dffrege115  44737  hbexg  45298  hbexgVD  45647  dfich2  48240  ichcom  48241