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

Theorem alcom 2161
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 2159 . 2 (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
2 ax-11 2159 . 2 (∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑)
31, 2impbii 212 1 (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wal 1536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-11 2159
This theorem depends on definitions:  df-bi 210
This theorem is referenced by:  alrot3  2162  sbal  2164  sbcom2  2166  excom  2167  nfa2  2175  sbnf2  2369  sbal1  2551  sbal2  2552  sbal2OLD  2553  2mo2  2712  ralcom4  3201  ralcom  3310  ralcomf  3313  unissb  4835  dfiin2g  4922  dftr5  5142  cotrg  5942  cnvsym  5945  dffun2  6338  fun11  6402  aceq1  9532  isch2  29009  moel  30262  dfon2lem8  33143  bj-hbaeb  34252  wl-sbcom2d  34955  wl-sbalnae  34956  wl-2spsbbi  34959  wl-dfralflem  34996  cocossss  35834  cossssid3  35862  trcoss2  35877  dford4  39957  elmapintrab  40263  undmrnresiss  40291  cnvssco  40293  elintima  40341  relexp0eq  40389  dfhe3  40463  dffrege115  40666  hbexg  41249  hbexgVD  41599  dfich2  43962  ichcom  43963
  Copyright terms: Public domain W3C validator