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

Theorem alcom 2022
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 2019 . 2 (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
2 ax-11 2019 . 2 (∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑)
31, 2impbii 197 1 (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-11 2019
This theorem depends on definitions:  df-bi 195
This theorem is referenced by:  alrot3  2023  excom  2026  sbnf2  2422  sbcom2  2428  sbal1  2443  sbal2  2444  2mo2  2533  ralcomf  3072  unissb  4395  dfiin2g  4479  dftr5  4673  cotrg  5409  cnvsym  5412  dffun2  5796  fun11  5859  aceq1  8796  isch2  27266  moel  28509  dfon2lem8  30741  bj-ssb1  31624  bj-hbaeb  31803  bj-ralcom4  31861  wl-sbcom2d  32322  wl-sbalnae  32323  dford4  36413  elmapintrab  36700  undmrnresiss  36728  cnvssco  36730  elintima  36763  relexp0eq  36811  dfhe3  36888  dffrege115  37091  hbexg  37592  hbexgVD  37963
  Copyright terms: Public domain W3C validator