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

Theorem eqcoms 2432
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 2429 . 2  |-  ( B  =  A  <->  A  =  B )
2 eqcoms.1 . 2  |-  ( A  =  B  ->  ph )
31, 2sylbi 198 1  |-  ( B  =  A  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-cleq 2412
This theorem is referenced by:  gencbvex  3122  sbceq2a  3308  eqimss2  3514  uneqdifeq  3881  tppreq3  4099  tpprceq3  4134  copsex2t  4700  copsex2g  4701  cnveqb  5303  cnveq0  5304  relcoi1OLD  5377  unixpid  5383  sspred  5399  funtpg  5643  f0rn0  5777  tz6.12i  5893  fveqdmss  6024  fvcofneq  6037  f1ocnvfv  6184  f1ocnvfvb  6185  cbvfo  6194  ov6g  6440  tfindsg  6693  findsg  6726  suppimacnv  6928  suppss  6948  ectocld  7430  ecoptocl  7453  undifixp  7558  phplem3  7751  f1dmvrnfibi  7856  f1vrnfibi  7857  card1  8399  pr2ne  8433  prdom2  8434  sornom  8703  indpi  9328  ltlen  9731  eqlei  9740  squeeze0  10505  nn0ind-raph  11031  injresinjlem  12017  hashf1rn  12528  hashrabsn1  12546  hash1snb  12584  hashgt12el  12586  hashgt12el2  12587  hash2prde  12621  hash2prd  12623  hash2pwpr  12624  brfi1uzind  12637  lswlgt0cl  12699  wrd2ind  12815  reuccats1lem  12817  swrdccatin12lem2  12826  swrdccatin12lem3  12827  swrdccat3a  12831  cshweqrep  12901  cshwsexa  12904  scshwfzeqfzo  12906  2swrd2eqwrdeq  13007  wwlktovfo  13012  rennim  13281  absmod0  13345  modfsummods  13831  m1dvdsndvds  14727  cshwrepswhash1  15051  xpsfrnel2  15449  initoeu2lem1  15887  istos  16259  symgfvne  17007  symgfix2  17035  symgextf1  17040  symgfixelsi  17054  psgnsn  17139  odbezout  17187  cntzcmnss  17459  frgpnabllem1  17487  psgndiflemB  19145  uvcendim  19382  mamufacex  19391  smatvscl  19526  mavmulsolcl  19553  mdetunilem8  19621  pm2mpfo  19815  chpscmat  19843  chmaidscmat  19849  chfacfscmulgsum  19861  chfacfpmmulgsum  19865  txcn  20618  qtopeu  20708  reeff1o  23379  relogbcxpb  23701  pntrlog2bndlem5  24396  usgraedg4  25091  usgraidx2vlem2  25096  nbgraf1olem5  25149  nb3graprlem1  25155  cusgrasize2inds  25181  usgrasscusgra  25187  wlkn0  25231  2pthlem2  25302  wlkdvspthlem  25313  usgra2wlkspthlem1  25323  fargshiftfv  25339  fargshiftf  25340  usgrcyclnl1  25344  usgrcyclnl2  25345  3v3e3cycl1  25348  constr3trllem2  25355  4cycl4v4e  25370  4cycl4dv4e  25372  wwlkn0  25393  wlkiswwlk1  25394  wlkiswwlk2lem3  25397  wlklniswwlkn1  25403  usg2wlkeq  25412  wwlknextbi  25429  wwlknredwwlkn0  25431  wwlkextwrd  25432  wwlkextsur  25435  wwlkextprop  25448  clwlkisclwwlklem2a4  25488  clwlkisclwwlklem2a  25489  clwwlkel  25497  clwwlkfo  25501  wwlkext2clwwlk  25507  clwwnisshclwwn  25513  eleclclwwlknlem2  25522  erclwwlkneqlen  25528  erclwwlkntr  25531  hashecclwwlkn1  25538  usghashecclwwlk  25539  clwlkfclwwlk  25548  clwlkfoclwwlk  25549  el2wlkonot  25573  el2spthonot  25574  el2spthonot0  25575  el2wlkonotot0  25576  el2wlkonotot1  25578  usg2spthonot0  25593  vdusgra0nedg  25612  usgravd0nedg  25622  rusgraprop2  25646  clwlknclwlkdifs  25664  eupatrl  25672  1to2vfriswmgra  25710  frgrancvvdeqlem3  25736  frgrancvvdeqlem4  25737  frgrancvvdeqlemB  25742  frgrancvvdeqlemC  25743  usgreghash2spotv  25770  extwwlkfablem1  25778  extwwlkfablem2  25782  numclwwlkun  25783  numclwlk1lem2f1  25798  numclwwlk2lem1  25806  numclwlk2lem2f  25807  ismgmOLD  26024  rngodm1dm2  26122  rngomndo  26125  rngoueqz  26134  zerdivemp1  26138  cdj1i  28062  brabgaf  28196  br8d  28198  sgn3da  29401  mthmb  30208  br8  30384  br4  30386  bj-snsetex  31507  bj-snglc  31513  poimirlem20  31868  poimirlem26  31874  poimirlem27  31875  mblfinlem3  31887  mblfinlem4  31888  itg2addnclem  31901  indexdom  31969  zerdivemp1x  32102  opcon3b  32675  ps-1  32955  3atlem5  32965  4atex  33554  pm13.192  36613  iotavalsb  36636  fourierdlem32  37789  fourierdlem49  37806  fourierdlem64  37821  nvelim  38242  fveqvfvv  38246  funressnfv  38250  afvpcfv0  38268  afv0nbfvbi  38273  fnbrafvb  38276  tz6.12-afv  38295  afvco2  38298  ndmaovg  38306  elprneb  38332  mod2eq1n2dvds  38345  iccpartiltu  38356  nn0o1gt2ALTV  38443  bgoldbwt  38498  nnsum4primeseven  38515  nnsum4primesevenALTV  38516  proththd  38534  lswn0  38540  pfxsuffeqwrdeq  38567  pfxccatin12lem2  38585  funopsn  38625  fzoopth  38659  usgra2pth  38730  usgvincvad  38778  usgvincvadALT  38781  usgfis  38820  usgfisALT  38824  lmod0rng  38930  lidldomn1  38983  zlidlring  38990  rngcinv  39045  rngcinvALTV  39057  ringcinv  39096  ringcinvALTV  39120  ztprmneprm  39192  lincext3  39313  zlmodzxznm  39354  suppdm  39368  elfzolborelfzop1  39381  nn0o1gt2  39392  nn0sumshdiglemB  39496
  Copyright terms: Public domain W3C validator