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  3261  ralcom  3263  ralcomf  3274  sbccomlem  3829  unissbOLD  4900  dfiin2g  4991  dftr5OLD  5214  cotrgOLD  6070  cnvsymOLD  6074  cnvsymOLDOLD  6075  dffun2OLD  6510  fun11  6574  aceq1  10046  isch2  31125  dfon2lem8  35751  bj-hbaeb  36780  wl-sb9v  37510  wl-sbcom2d  37522  wl-sbalnae  37523  wl-2spsbbi  37526  cocossss  38400  cossssid3  38433  trcoss2  38448  dford4  42991  unielss  43180  elmapintrab  43538  undmrnresiss  43566  cnvssco  43568  elintima  43615  relexp0eq  43663  dfhe3  43737  dffrege115  43940  hbexg  44519  hbexgVD  44868  dfich2  47432  ichcom  47433