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  2368  sb8v  2388  sb8f  2389  sbnf2  2393  sbal1  2563  sbal2  2564  2mo2  2678  ralcom4  3294  ralcom  3296  ralcomf  3306  sbccomlem  3825  dfiin2g  4998  fun11  6614  aceq1  10112  isch2  31590  dfon2lem8  36292  bj-hbaeb  37486  bj-axseprep  37743  wl-sb9v  38236  wl-sbcom2d  38248  wl-sbalnae  38249  wl-2spsbbi  38252  cocossss  39207  cossssid3  39240  trcoss2  39255  dford4  43788  unielss  43977  elmapintrab  44334  undmrnresiss  44362  cnvssco  44364  elintima  44411  relexp0eq  44459  dfhe3  44533  dffrege115  44736  hbexg  45297  hbexgVD  45646  dfich2  48239  ichcom  48240