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

Theorem alcom 2153
Description: Theorem 19.5 of [Margaris] p. 89. (Contributed by NM, 30-Jun-1993.)
Assertion
Ref Expression
alcom (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)

Proof of Theorem alcom
StepHypRef Expression
1 ax-11 2151 . 2 (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
2 ax-11 2151 . 2 (∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑)
31, 2impbii 210 1 (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-11 2151
This theorem depends on definitions:  df-bi 208
This theorem is referenced by:  alrot3  2154  sbal  2156  sbcom2  2158  excom  2159  nfa2  2166  sbnf2  2368  sbal1  2565  sbal2  2566  sbal2OLD  2567  2mo2  2725  ralcom4  3232  ralcom  3351  ralcomf  3354  unissb  4861  dfiin2g  4948  dftr5  5166  cotrg  5964  cnvsym  5967  dffun2  6358  fun11  6421  aceq1  9531  isch2  28927  moel  30179  dfon2lem8  32932  bj-hbaeb  34039  wl-sbcom2d  34678  wl-sbalnae  34679  wl-2spsbbi  34682  wl-dfralflem  34719  cocossss  35561  cossssid3  35589  trcoss2  35604  dford4  39504  elmapintrab  39814  undmrnresiss  39842  cnvssco  39844  elintima  39876  relexp0eq  39924  dfhe3  39999  dffrege115  40202  hbexg  40767  hbexgVD  41117  dfich2  43490  dfich2ai  43491  ichcom  43494
  Copyright terms: Public domain W3C validator