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  3263  ralcom  3265  ralcomf  3276  sbccomlem  3832  unissbOLD  4904  dfiin2g  4996  dftr5OLD  5219  cotrgOLD  6081  cotrgOLDOLD  6082  cnvsymOLD  6086  cnvsymOLDOLD  6087  dffun2OLD  6522  dffun2OLDOLD  6523  fun11  6590  aceq1  10070  isch2  31152  dfon2lem8  35778  bj-hbaeb  36807  wl-sb9v  37537  wl-sbcom2d  37549  wl-sbalnae  37550  wl-2spsbbi  37553  cocossss  38427  cossssid3  38460  trcoss2  38475  dford4  43018  unielss  43207  elmapintrab  43565  undmrnresiss  43593  cnvssco  43595  elintima  43642  relexp0eq  43690  dfhe3  43764  dffrege115  43967  hbexg  44546  hbexgVD  44895  dfich2  47459  ichcom  47460