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

Theorem alcom 2024
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 2021 . 2 (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
2 ax-11 2021 . 2 (∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑)
31, 2impbii 198 1 (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wal 1473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-11 2021
This theorem depends on definitions:  df-bi 196
This theorem is referenced by:  alrot3  2025  nfa2  2027  excom  2029  sbnf2  2427  sbcom2  2433  sbal1  2448  sbal2  2449  2mo2  2538  ralcomf  3077  unissb  4405  dfiin2g  4489  dftr5  4683  cotrg  5426  cnvsym  5429  dffun2  5814  fun11  5877  aceq1  8823  isch2  27464  moel  28707  dfon2lem8  30939  bj-ssb1  31822  bj-hbaeb  31994  bj-ralcom4  32062  wl-sbcom2d  32523  wl-sbalnae  32524  dford4  36614  elmapintrab  36901  undmrnresiss  36929  cnvssco  36931  elintima  36964  relexp0eq  37012  dfhe3  37089  dffrege115  37292  hbexg  37793  hbexgVD  38164
  Copyright terms: Public domain W3C validator