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

Theorem eqcoms 2458
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 2457 . 2  |-  ( B  =  A  <->  A  =  B )
2 eqcoms.1 . 2  |-  ( A  =  B  ->  ph )
31, 2sylbi 199 1  |-  ( B  =  A  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1443
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-cleq 2443
This theorem is referenced by:  gencbvex  3091  sbceq2a  3278  eqimss2  3484  uneqdifeq  3855  tppreq3  4076  tpprceq3  4111  copsex2t  4687  copsex2g  4688  cnveqb  5290  cnveq0  5291  relcoi1OLD  5364  unixpid  5370  sspred  5387  funtpg  5631  f0rn0  5766  tz6.12i  5883  fveqdmss  6015  fvcofneq  6028  f1ocnvfv  6175  f1ocnvfvb  6176  cbvfo  6185  ov6g  6431  tfindsg  6684  findsg  6717  suppimacnv  6922  suppss  6942  ectocld  7427  ecoptocl  7450  undifixp  7555  phplem3  7750  f1dmvrnfibi  7855  f1vrnfibi  7856  card1  8399  pr2ne  8433  prdom2  8434  sornom  8704  indpi  9329  ltlen  9732  eqlei  9741  squeeze0  10506  nn0ind-raph  11032  injresinjlem  12021  hashf1rn  12532  hashrabsn1  12550  hash1snb  12590  hashgt12el  12592  hashgt12el2  12593  hash2prde  12628  hash2pwpr  12632  fi1uzind  12647  brfi1indALT  12650  lswlgt0cl  12713  wrd2ind  12829  reuccats1lem  12831  swrdccatin12lem2  12840  swrdccatin12lem3  12841  swrdccat3a  12845  cshweqrep  12915  cshwsexa  12918  scshwfzeqfzo  12920  2swrd2eqwrdeq  13021  wwlktovfo  13026  rennim  13295  absmod0  13359  modfsummods  13846  m1dvdsndvds  14742  cshwrepswhash1  15066  xpsfrnel2  15464  initoeu2lem1  15902  istos  16274  symgfvne  17022  symgfix2  17050  symgextf1  17055  symgfixelsi  17069  psgnsn  17154  odbezout  17202  cntzcmnss  17474  frgpnabllem1  17502  psgndiflemB  19161  uvcendim  19398  mamufacex  19407  smatvscl  19542  mavmulsolcl  19569  mdetunilem8  19637  pm2mpfo  19831  chpscmat  19859  chmaidscmat  19865  chfacfscmulgsum  19877  chfacfpmmulgsum  19881  txcn  20634  qtopeu  20724  reeff1o  23395  relogbcxpb  23717  pntrlog2bndlem5  24412  usgraedg4  25107  usgraidx2vlem2  25112  nbgraf1olem5  25166  nb3graprlem1  25172  cusgrasize2inds  25198  usgrasscusgra  25204  wlkn0  25248  2pthlem2  25319  wlkdvspthlem  25330  usgra2wlkspthlem1  25340  fargshiftfv  25356  fargshiftf  25357  usgrcyclnl1  25361  usgrcyclnl2  25362  3v3e3cycl1  25365  constr3trllem2  25372  4cycl4v4e  25387  4cycl4dv4e  25389  wwlkn0  25410  wlkiswwlk1  25411  wlkiswwlk2lem3  25414  wlklniswwlkn1  25420  usg2wlkeq  25429  wwlknextbi  25446  wwlknredwwlkn0  25448  wwlkextwrd  25449  wwlkextsur  25452  wwlkextprop  25465  clwlkisclwwlklem2a4  25505  clwlkisclwwlklem2a  25506  clwwlkel  25514  clwwlkfo  25518  wwlkext2clwwlk  25524  clwwnisshclwwn  25530  eleclclwwlknlem2  25539  erclwwlkneqlen  25545  erclwwlkntr  25548  hashecclwwlkn1  25555  usghashecclwwlk  25556  clwlkfclwwlk  25565  clwlkfoclwwlk  25566  el2wlkonot  25590  el2spthonot  25591  el2spthonot0  25592  el2wlkonotot0  25593  el2wlkonotot1  25595  usg2spthonot0  25610  vdusgra0nedg  25629  usgravd0nedg  25639  rusgraprop2  25663  clwlknclwlkdifs  25681  eupatrl  25689  1to2vfriswmgra  25727  frgrancvvdeqlem3  25753  frgrancvvdeqlem4  25754  frgrancvvdeqlemB  25759  frgrancvvdeqlemC  25760  usgreghash2spotv  25787  extwwlkfablem1  25795  extwwlkfablem2  25799  numclwwlkun  25800  numclwlk1lem2f1  25815  numclwwlk2lem1  25823  numclwlk2lem2f  25824  ismgmOLD  26041  rngodm1dm2  26139  rngomndo  26142  rngoueqz  26151  zerdivemp1  26155  cdj1i  28079  brabgaf  28209  br8d  28211  sgn3da  29405  mthmb  30212  br8  30389  br4  30391  bj-snsetex  31550  bj-snglc  31556  poimirlem20  31953  poimirlem26  31959  poimirlem27  31960  mblfinlem3  31972  mblfinlem4  31973  itg2addnclem  31986  indexdom  32054  zerdivemp1x  32187  opcon3b  32756  ps-1  33036  3atlem5  33046  4atex  33635  pm13.192  36755  iotavalsb  36778  fourierdlem32  37996  fourierdlem49  38013  fourierdlem64  38028  nvelim  38615  fveqvfvv  38619  funressnfv  38623  afvpcfv0  38642  afv0nbfvbi  38647  fnbrafvb  38650  tz6.12-afv  38669  afvco2  38672  ndmaovg  38680  elprneb  38706  mod2eq1n2dvds  38719  iccpartiltu  38730  nn0o1gt2ALTV  38817  bgoldbwt  38872  nnsum4primeseven  38889  nnsum4primesevenALTV  38890  proththd  38908  lswn0  38914  pfxsuffeqwrdeq  38941  pfxccatin12lem2  38959  elpr2elpr  38997  funopsn  39012  f1ssf1  39015  riotaeqimp  39024  fzoopth  39050  usgredg2vlem2  39289  ushgredgedga  39292  ushgredgedgaloop  39294  usgredgaleordALT  39297  uhgrspan1  39358  nb3grprlem1  39437  uvtxnbgrb  39457  cplgruvtxb  39466  cusgrsize2inds  39497  rusgrpropnb  39582  1wlkn0  39618  1wlkvtxiedg  39620  wlk1wlk  39632  upgr1wlkvtxedg  39637  0wlkOn  39649  usgra2pth  39655  usgvincvad  39703  usgvincvadALT  39706  usgfis  39745  usgfisALT  39749  lmod0rng  39855  lidldomn1  39908  zlidlring  39915  rngcinv  39970  rngcinvALTV  39982  ringcinv  40021  ringcinvALTV  40045  ztprmneprm  40115  lincext3  40236  zlmodzxznm  40277  suppdm  40291  elfzolborelfzop1  40303  nn0o1gt2  40314  nn0sumshdiglemB  40418
  Copyright terms: Public domain W3C validator