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

Theorem eqcoms 2414
Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 24-Jun-1993.)
Hypothesis
Ref Expression
eqcoms.1  |-  ( A  =  B  ->  ph )
Assertion
Ref Expression
eqcoms  |-  ( B  =  A  ->  ph )

Proof of Theorem eqcoms
StepHypRef Expression
1 eqcom 2411 . 2  |-  ( B  =  A  <->  A  =  B )
2 eqcoms.1 . 2  |-  ( A  =  B  ->  ph )
31, 2sylbi 195 1  |-  ( B  =  A  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-cleq 2394
This theorem is referenced by:  gencbvex  3102  sbceq2a  3288  eqimss2  3494  uneqdifeq  3859  tppreq3  4076  tpprceq3  4111  copsex2t  4676  copsex2g  4677  cnveqb  5278  cnveq0  5279  relcoi1OLD  5352  unixpid  5358  sspred  5374  funtpg  5618  f0rn0  5752  tz6.12i  5868  fveqdmss  6003  fvcofneq  6016  f1ocnvfv  6164  f1ocnvfvb  6165  cbvfo  6174  ov6g  6420  tfindsg  6677  findsg  6710  suppimacnv  6912  suppss  6932  ectocld  7414  ecoptocl  7437  undifixp  7542  phplem3  7735  card1  8380  pr2ne  8414  prdom2  8415  sornom  8688  indpi  9314  ltlen  9716  eqlei  9725  squeeze0  10487  nn0ind-raph  11002  injresinjlem  11960  hashf1rn  12470  hashrabsn1  12488  hash1snb  12526  hashgt12el  12528  hashgt12el2  12529  hash2prde  12563  hash2prd  12565  hash2pwpr  12566  brfi1uzind  12579  lswlgt0cl  12641  wrd2ind  12757  reuccats1lem  12759  swrdccatin12lem2  12768  swrdccatin12lem3  12769  swrdccat3a  12773  cshweqrep  12843  cshwsexa  12846  scshwfzeqfzo  12848  2swrd2eqwrdeq  12945  wwlktovfo  12950  rennim  13219  absmod0  13283  modfsummods  13756  m1dvdsndvds  14532  cshwrepswhash1  14794  xpsfrnel2  15177  initoeu2lem1  15615  istos  15987  symgfvne  16735  symgfix2  16763  symgextf1  16768  symgfixelsi  16782  psgnsn  16867  odbezout  16902  cntzcmnss  17171  frgpnabllem1  17199  psgndiflemB  18932  uvcendim  19172  mamufacex  19181  smatvscl  19316  mavmulsolcl  19343  mdetunilem8  19411  pm2mpfo  19605  chpscmat  19633  chmaidscmat  19639  chfacfscmulgsum  19651  chfacfpmmulgsum  19655  txcn  20417  qtopeu  20507  reeff1o  23132  relogbcxpb  23452  pntrlog2bndlem5  24145  usgraedg4  24791  usgraidx2vlem2  24796  nbgraf1olem5  24849  nb3graprlem1  24855  cusgrasize2inds  24881  usgrasscusgra  24887  wlkn0  24931  2pthlem2  25002  wlkdvspthlem  25013  usgra2wlkspthlem1  25023  fargshiftfv  25039  fargshiftf  25040  usgrcyclnl1  25044  usgrcyclnl2  25045  3v3e3cycl1  25048  constr3trllem2  25055  4cycl4v4e  25070  4cycl4dv4e  25072  wwlkn0  25093  wlkiswwlk1  25094  wlkiswwlk2lem3  25097  wlklniswwlkn1  25103  usg2wlkeq  25112  wwlknextbi  25129  wwlknredwwlkn0  25131  wwlkextwrd  25132  wwlkextsur  25135  wwlkextprop  25148  clwlkisclwwlklem2a4  25188  clwlkisclwwlklem2a  25189  clwwlkel  25197  clwwlkfo  25201  wwlkext2clwwlk  25207  clwwnisshclwwn  25213  eleclclwwlknlem2  25222  erclwwlkneqlen  25228  erclwwlkntr  25231  hashecclwwlkn1  25238  usghashecclwwlk  25239  clwlkfclwwlk  25248  clwlkfoclwwlk  25249  el2wlkonot  25273  el2spthonot  25274  el2spthonot0  25275  el2wlkonotot0  25276  el2wlkonotot1  25278  usg2spthonot0  25293  vdusgra0nedg  25312  usgravd0nedg  25322  rusgraprop2  25346  clwlknclwlkdifs  25364  eupatrl  25372  1to2vfriswmgra  25410  frgrancvvdeqlem3  25436  frgrancvvdeqlem4  25437  frgrancvvdeqlemB  25442  frgrancvvdeqlemC  25443  usgreghash2spotv  25470  extwwlkfablem1  25478  extwwlkfablem2  25482  numclwwlkun  25483  numclwlk1lem2f1  25498  numclwwlk2lem1  25506  numclwlk2lem2f  25507  ismgmOLD  25722  rngodm1dm2  25820  rngomndo  25823  rngoueqz  25832  zerdivemp1  25836  cdj1i  27751  brabgaf  27884  br8d  27886  sgn3da  28972  mthmb  29780  br8  29956  br4  29958  bj-snsetex  31073  bj-snglc  31079  mblfinlem3  31405  mblfinlem4  31406  itg2addnclem  31419  indexdom  31487  zerdivemp1x  31620  opcon3b  32194  ps-1  32474  3atlem5  32484  4atex  33073  pm13.192  36145  iotavalsb  36168  fourierdlem32  37270  fourierdlem49  37287  fourierdlem64  37302  nvelim  37554  fveqvfvv  37558  funressnfv  37562  afvpcfv0  37580  afv0nbfvbi  37585  fnbrafvb  37588  tz6.12-afv  37607  afvco2  37610  ndmaovg  37618  elprneb  37644  mod2eq1n2dvds  37657  iccpartiltu  37670  nn0o1gt2ALTV  37757  bgoldbwt  37812  nnsum4primeseven  37829  nnsum4primesevenALTV  37830  proththd  37841  lswn0  37847  pfxsuffeqwrdeq  37874  pfxccatin12lem2  37892  f1dmvrnfibi  37926  f1vrnfibi  37927  fzoopth  37952  usgra2pth  37964  usgvincvad  38014  usgvincvadALT  38017  usgfis  38056  usgfisALT  38060  lmod0rng  38166  lidldomn1  38219  zlidlring  38226  rngcinv  38281  rngcinvALTV  38293  ringcinv  38332  ringcinvALTV  38356  ztprmneprm  38428  lincext3  38549  zlmodzxznm  38590  suppdm  38604  elfzolborelfzop1  38617  nn0o1gt2  38628  nn0sumshdiglemB  38732
  Copyright terms: Public domain W3C validator