Theorem alcom 2160

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

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 206  ∀wal 1538

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  alrot3  2161  excom  2163  sbal  2170  sbcom2  2174  nfa2  2177  aaan  2331  sb8v  2351  sb8f  2352  sbnf2  2356  sbal1  2526  sbal2  2527  2mo2  2640  ralcom4  3255  ralcom  3257  ralcomf  3268  sbccomlem  3823  dfiin2g  4984  fun11  6560  aceq1  10030  isch2  31185  dfon2lem8  35766  bj-hbaeb  36795  wl-sb9v  37525  wl-sbcom2d  37537  wl-sbalnae  37538  wl-2spsbbi  37541  cocossss  38415  cossssid3  38448  trcoss2  38463  dford4  43005  unielss  43194  elmapintrab  43552  undmrnresiss  43580  cnvssco  43582  elintima  43629  relexp0eq  43677  dfhe3  43751  dffrege115  43954  hbexg  44533  hbexgVD  44882  dfich2  47446  ichcom  47447