Theorem alcom 2192

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

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 208  ∀wal 1557

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

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  alrot3  2193  excom  2195  sbal  2202  sbcom2  2205  nfa2  2208  aaan  2363  sb8v  2383  sb8f  2384  sbnf2  2388  sbal1  2558  sbal2  2559  2mo2  2673  ralcom4  3287  ralcom  3289  ralcomf  3299  sbccomlem  3820  dfiin2g  4985  fun11  6590  aceq1  10067  isch2  31383  dfon2lem8  36099  bj-hbaeb  37265  bj-axseprep  37520  wl-sb9v  38013  wl-sbcom2d  38025  wl-sbalnae  38026  wl-2spsbbi  38029  cocossss  38986  cossssid3  39019  trcoss2  39034  dford4  43567  unielss  43756  elmapintrab  44113  undmrnresiss  44141  cnvssco  44143  elintima  44190  relexp0eq  44238  dfhe3  44312  dffrege115  44515  hbexg  45093  hbexgVD  45442  dfich2  48025  ichcom  48026