MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alcom Structured version   Visualization version   GIF version

Theorem alcom 2159
Description: Theorem 19.5 of [Margaris] p. 89. Use its weak version alcomw 2044 when it allows to avoid dependence on ax-11 2157. (Contributed by NM, 30-Jun-1993.)
Assertion
Ref Expression
alcom (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)

Proof of Theorem alcom
StepHypRef Expression
1 ax-11 2157 . 2 (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
2 ax-11 2157 . 2 (∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑)
31, 2impbii 209 1 (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)
Colors of variables: wff setvar class
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 2157
This theorem depends on definitions:  df-bi 207
This theorem is referenced by:  alrot3  2160  excom  2162  sbal  2169  sbcom2  2173  nfa2  2176  aaan  2333  sb8v  2355  sb8f  2356  sbnf2  2361  sbal1  2533  sbal2  2534  2mo2  2647  ralcom4  3286  ralcom4OLD  3287  ralcom  3289  nfra2wOLD  3300  ralcomf  3302  moelOLD  3405  sbccomlem  3869  unissbOLD  4940  dfiin2g  5032  dftr5OLD  5264  cotrgOLD  6128  cotrgOLDOLD  6129  cnvsymOLD  6133  cnvsymOLDOLD  6134  dffun2OLD  6572  dffun2OLDOLD  6573  fun11  6640  aceq1  10157  isch2  31242  dfon2lem8  35791  bj-hbaeb  36820  wl-sb9v  37550  wl-sbcom2d  37562  wl-sbalnae  37563  wl-2spsbbi  37566  cocossss  38437  cossssid3  38470  trcoss2  38485  dford4  43041  unielss  43230  elmapintrab  43589  undmrnresiss  43617  cnvssco  43619  elintima  43666  relexp0eq  43714  dfhe3  43788  dffrege115  43991  hbexg  44576  hbexgVD  44926  dfich2  47445  ichcom  47446
  Copyright terms: Public domain W3C validator