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

Theorem eqcoms 2455
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 2452 . 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 1383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435
This theorem is referenced by:  gencbvex  3139  sbceq2a  3325  eqimss2  3542  uneqdifeq  3902  tppreq3  4120  tpprceq3  4155  copsex2t  4724  copsex2g  4725  cnveqb  5452  cnveq0  5453  relcoi1  5526  unixpid  5532  funtpg  5628  f0rn0  5760  tz6.12i  5876  fveqdmss  6011  fvcofneq  6024  f1ocnvfv  6169  f1ocnvfvb  6170  cbvfo  6177  ov6g  6425  tfindsg  6680  findsg  6712  suppimacnv  6914  suppss  6932  ectocld  7380  ecoptocl  7403  undifixp  7507  phplem3  7700  card1  8352  pr2ne  8386  prdom2  8387  sornom  8660  indpi  9288  ltlen  9689  eqlei  9697  squeeze0  10455  nn0ind-raph  10971  injresinjlem  11907  hashf1rn  12407  hashrabsn1  12424  hash1snb  12461  hashgt12el  12463  hashgt12el2  12464  hash2prde  12498  hash2prd  12500  hash2pwpr  12501  brfi1uzind  12514  lswlgt0cl  12572  ccatw2s1p1  12622  ccatw2s1p2  12623  wrdeqswrdlsw  12656  wrd2ind  12685  reuccats1lem  12687  swrdccatin12lem2  12696  swrdccatin12lem3  12697  swrdccat3a  12701  cshweqrep  12771  cshwsexa  12774  scshwfzeqfzo  12776  2swrd2eqwrdeq  12873  wwlktovfo  12878  rennim  13054  absmod0  13118  modfsummods  13589  m1dvdsndvds  14307  cshwrepswhash1  14569  xpsfrnel2  14944  istos  15644  symgfvne  16392  symgfix2  16420  symgextf1  16425  symgfixelsi  16439  psgnsn  16524  odbezout  16559  cntzcmnss  16828  frgpnabllem1  16856  psgndiflemB  18614  uvcendim  18860  mamufacex  18869  smatvscl  19004  mavmulsolcl  19031  mdetunilem8  19099  pm2mpfo  19293  chpscmat  19321  chmaidscmat  19327  chfacfscmulgsum  19339  chfacfpmmulgsum  19343  bwthOLD  19889  txcn  20105  qtopeu  20195  reeff1o  22820  pntrlog2bndlem5  23744  usgraedg4  24365  usgraidx2vlem2  24370  nbgraf1olem5  24423  nb3graprlem1  24429  cusgrasize2inds  24455  usgrasscusgra  24461  wlkn0  24505  2pthlem2  24576  wlkdvspthlem  24587  usgra2wlkspthlem1  24597  fargshiftfv  24613  fargshiftf  24614  usgrcyclnl1  24618  usgrcyclnl2  24619  3v3e3cycl1  24622  constr3trllem2  24629  4cycl4v4e  24644  4cycl4dv4e  24646  wwlkn0  24667  wlkiswwlk1  24668  wlkiswwlk2lem3  24671  wlklniswwlkn1  24677  usg2wlkeq  24686  wwlknextbi  24703  wwlknredwwlkn0  24705  wwlkextwrd  24706  wwlkextsur  24709  wwlkextprop  24722  clwlkisclwwlklem2a4  24762  clwlkisclwwlklem2a  24763  clwwlkel  24771  clwwlkfo  24775  wwlkext2clwwlk  24781  clwwnisshclwwn  24787  eleclclwwlknlem2  24796  erclwwlkneqlen  24802  erclwwlkntr  24805  hashecclwwlkn1  24812  usghashecclwwlk  24813  clwlkfclwwlk  24822  clwlkfoclwwlk  24823  el2wlkonot  24847  el2spthonot  24848  el2spthonot0  24849  el2wlkonotot0  24850  el2wlkonotot1  24852  usg2spthonot0  24867  vdusgra0nedg  24886  usgravd0nedg  24896  rusgraprop2  24920  clwlknclwlkdifs  24938  eupatrl  24946  1to2vfriswmgra  24984  frgrancvvdeqlem3  25010  frgrancvvdeqlem4  25011  frgrancvvdeqlemB  25016  frgrancvvdeqlemC  25017  usgreghash2spotv  25044  extwwlkfablem1  25052  extwwlkfablem2  25056  numclwwlkun  25057  numclwlk1lem2f1  25072  numclwwlk2lem1  25080  numclwlk2lem2f  25081  ismgmOLD  25300  rngodm1dm2  25398  rngomndo  25401  rngoueqz  25410  zerdivemp1  25414  cdj1i  27330  br8d  27441  sgn3da  28458  mthmb  28919  br8  29161  br4  29163  sspred  29228  mblfinlem3  30029  mblfinlem4  30030  itg2addnclem  30042  indexdom  30201  zerdivemp1x  30334  pm13.192  31271  iotavalsb  31294  fourierdlem32  31875  fourierdlem49  31892  fourierdlem64  31907  nvelim  32159  fveqvfvv  32163  funressnfv  32167  afvpcfv0  32185  afv0nbfvbi  32190  fnbrafvb  32193  tz6.12-afv  32212  afvco2  32215  ndmaovg  32223  f1dmvrnfibi  32266  f1vrnfibi  32267  fzoopth  32294  lswn0  32297  usgra2pth  32308  usgvincvad  32358  usgvincvadALT  32361  usgfis  32400  usgfisALT  32404  lidldomn1  32554  zlidlring  32561  rngcinv  32664  rngcinvOLD  32676  ringcinv  32712  ringcinvOLD  32736  ztprmneprm  32804  lmod0rng  32829  lincext3  32927  zlmodzxznm  32968  bj-snsetex  34404  bj-snglc  34410  opcon3b  34796  ps-1  35076  3atlem5  35086  4atex  35675
  Copyright terms: Public domain W3C validator