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

Theorem alcom 2095
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 2093 . 2 (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
2 ax-11 2093 . 2 (∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑)
31, 2impbii 201 1 (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 198  wal 1505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-11 2093
This theorem depends on definitions:  df-bi 199
This theorem is referenced by:  alrot3  2096  excom  2098  nfa2  2105  sbnf2  2291  sbcom2  2410  sbcom2OLD  2411  sbal1  2495  sbal2  2496  sbal2OLD  2497  sbal2OLDOLD  2498  sbal  2499  nexmoOLD  2549  2mo2  2679  ralcom4  3183  ralcom  3296  ralcomf  3299  unissb  4743  dfiin2g  4827  dftr5  5033  cotrg  5811  cnvsym  5814  dffun2  6198  fun11  6261  aceq1  9337  isch2  28779  moel  30034  dfon2lem8  32552  bj-hbaeb  33630  wl-sbcom2d  34235  wl-sbalnae  34236  wl-2spsbbi  34239  wl-dfralflem  34276  cocossss  35123  cossssid3  35151  trcoss2  35166  dford4  39019  elmapintrab  39295  undmrnresiss  39323  cnvssco  39325  elintima  39358  relexp0eq  39406  dfhe3  39481  dffrege115  39684  hbexg  40306  hbexgVD  40656  dfich2  42981  dfich2ai  42982  ichcom  42985
  Copyright terms: Public domain W3C validator