Theorem alcom 2154

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

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 205  ∀wal 1537

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  alrot3  2155  sbal  2157  sbcom2  2159  excom  2160  nfa2  2168  aaan  2325  sb8v  2346  sb8f  2347  sbnf2  2352  sbal1  2525  sbal2  2526  2mo2  2641  ralcom4  3281  ralcom4OLD  3282  ralcom  3284  nfra2wOLD  3295  ralcomf  3297  moelOLD  3399  unissbOLD  4945  dfiin2g  5036  dftr5OLD  5271  cotrgOLD  6110  cotrgOLDOLD  6111  cnvsymOLD  6115  cnvsymOLDOLD  6116  dffun2OLD  6555  dffun2OLDOLD  6556  fun11  6623  aceq1  10116  isch2  30741  dfon2lem8  35064  bj-hbaeb  36002  wl-sbcom2d  36731  wl-sbalnae  36732  wl-2spsbbi  36735  cocossss  37611  cossssid3  37644  trcoss2  37659  dford4  42072  unielss  42271  elmapintrab  42631  undmrnresiss  42659  cnvssco  42661  elintima  42708  relexp0eq  42756  dfhe3  42830  dffrege115  43033  hbexg  43621  hbexgVD  43971  dfich2  46426  ichcom  46427