MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  equcom Unicode version

Theorem equcom 1794
Description: Commutative law for equality. (Contributed by NM, 20-Aug-1993.)
Assertion
Ref Expression
equcom

Proof of Theorem equcom
StepHypRef Expression
1 equcomi 1793 . 2
2 equcomi 1793 . 2
31, 2impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  equequ2  1799  equvin  1804  dvelimhw  1955  nfeqf1  2043  eu1  2327  2eu6OLD  2384  reu7  3294  reu8  3295  iunid  4385  disjxun  4450  copsexg  4737  copsexgOLD  4738  opelopabsbALT  4761  dfid3  4801  opeliunxp  5056  relop  5158  dmi  5222  opabresid  5332  restidsing  5335  asymref2  5389  intirr  5390  cnvi  5415  coi1  5528  cnvso  5551  brprcneu  5864  dffv2  5946  fvn0ssdmfun  6022  f1oiso  6247  qsid  7396  mapsnen  7613  marypha2lem2  7916  dfac5lem2  8526  dfac5lem3  8527  kmlem15  8565  brdom7disj  8930  suplem2pr  9452  wloglei  10110  fimaxre  10515  arch  10817  dflt2  11383  hashgt12el  12481  hashge2el2dif  12521  summo  13539  tosso  15666  opsrtoslem1  18148  mamulid  18943  mpt2matmul  18948  mattpos1  18958  scmatscm  19015  1marepvmarrepid  19077  ist1-3  19850  unisngl  20028  cnmptid  20162  fmid  20461  tgphaus  20615  dscopn  21094  iundisj2  21959  dvlip  22394  ply1divmo  22536  frg2wot1  25057  disjabrex  27443  disjabrexf  27444  iundisj2f  27449  iundisj2fi  27602  ordtconlem1  27906  ghomf1olem  29034  dfid4  29103  dfdm5  29206  dfrn5  29207  dffun10  29564  elfuns  29565  dfiota3  29573  brimg  29587  dfrdg4  29600  wl-equsalcom  29995  nn0prpwlem  30140  eq0rabdioph  30710  opeliun2xp  32922  relopabVD  33701  bj-equcomd  34234  pmapglb  35494  polval2N  35630  diclspsn  36921
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator