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

Theorem alcom 2205
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 2202 . 2 (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
2 ax-11 2202 . 2 (∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑)
31, 2impbii 200 1 (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wal 1635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-11 2202
This theorem depends on definitions:  df-bi 198
This theorem is referenced by:  alrot3  2206  nfa2  2208  excom  2210  sbnf2  2604  sbcom2  2608  sbal1  2623  sbal2  2624  nexmo  2640  2mo2  2725  ralcomf  3295  unissb  4674  dfiin2g  4756  dftr5  4960  cotrg  5731  cnvsym  5735  dffun2  6121  fun11  6184  aceq1  9233  isch2  28431  moel  29674  dfon2lem8  32037  bj-ssb1  32971  bj-hbaeb  33138  bj-ralcom4  33195  wl-sbcom2d  33677  wl-sbalnae  33678  cocossss  34523  cossssid3  34551  trcoss2  34566  dford4  38115  elmapintrab  38400  undmrnresiss  38428  cnvssco  38430  elintima  38463  relexp0eq  38511  dfhe3  38587  dffrege115  38790  hbexg  39288  hbexgVD  39654
  Copyright terms: Public domain W3C validator