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

Theorem alcom 2034
 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 2031 . 2 (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
2 ax-11 2031 . 2 (∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑)
31, 2impbii 199 1 (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196  ∀wal 1478 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-11 2031 This theorem depends on definitions:  df-bi 197 This theorem is referenced by:  alrot3  2035  nfa2  2037  excom  2039  sbnf2  2438  sbcom2  2444  sbal1  2459  sbal2  2460  2mo2  2549  ralcomf  3090  unissb  4442  dfiin2g  4526  dftr5  4725  cotrg  5476  cnvsym  5479  dffun2  5867  fun11  5931  aceq1  8900  isch2  27968  moel  29212  dfon2lem8  31449  bj-ssb1  32328  bj-hbaeb  32502  bj-ralcom4  32568  wl-sbcom2d  33015  wl-sbalnae  33016  dford4  37115  elmapintrab  37402  undmrnresiss  37430  cnvssco  37432  elintima  37465  relexp0eq  37513  dfhe3  37590  dffrege115  37793  hbexg  38293  hbexgVD  38664
 Copyright terms: Public domain W3C validator