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

Theorem eqcoms 2479
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 2476 . 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 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  gencbvex  3157  sbceq2a  3343  eqimss2  3557  uneqdifeq  3915  tppreq3  4132  tpprceq3  4167  copsex2t  4734  copsex2g  4735  cnveqb  5461  cnveq0  5462  relcoi1  5535  unixpid  5541  funtpg  5637  f0rn0  5769  tz6.12i  5885  fvcofneq  6028  f1ocnvfv  6171  f1ocnvfvb  6172  cbvfo  6179  ov6g  6423  tfindsg  6674  findsg  6706  suppimacnv  6912  suppss  6930  ectocld  7378  ecoptocl  7401  undifixp  7505  phplem3  7698  card1  8348  pr2ne  8382  prdom2  8383  sornom  8656  indpi  9284  ltlen  9685  eqlei  9693  squeeze0  10447  nn0ind-raph  10960  injresinjlem  11892  hashf1rn  12392  hashrabsn1  12409  hash1snb  12443  euhash1  12444  hashgt12el  12445  hashgt12el2  12446  hash2prde  12481  hash2prd  12483  hash2pwpr  12484  brfi1uzind  12497  lswlgt0cl  12554  ccatw2s1p1  12602  ccatw2s1p2  12603  wrdeqswrdlsw  12636  wrd2ind  12665  reuccats1lem  12667  swrdccatin12lem2  12676  swrdccatin12lem3  12677  swrdccat3a  12681  cshweqrep  12751  cshwsexa  12754  scshwfzeqfzo  12756  2swrd2eqwrdeq  12853  wwlktovfo  12858  rennim  13034  absmod0  13098  modfsummods  13569  m1dvdsndvds  14183  cshwrepswhash1  14444  xpsfrnel2  14819  istos  15521  symgfvne  16215  symgfix2  16243  symgextf1  16248  symgfixelsi  16262  psgnsn  16348  odbezout  16383  cntzcmnss  16649  frgpnabllem1  16677  psgndiflemB  18419  uvcendim  18665  mamufacex  18674  smatvscl  18809  mavmulsolcl  18836  mdetunilem8  18904  pm2mpfo  19098  chpscmat  19126  chmaidscmat  19132  chfacfscmulgsum  19144  chfacfpmmulgsum  19148  bwthOLD  19693  txcn  19878  qtopeu  19968  reeff1o  22592  pntrlog2bndlem5  23510  usgraedg4  24079  usgraidx2vlem2  24084  nbgraf1olem5  24137  nb3graprlem1  24143  cusgrasize2inds  24169  usgrasscusgra  24175  wlkn0  24219  2pthlem2  24290  wlkdvspthlem  24301  usgra2wlkspthlem1  24311  fargshiftfv  24327  fargshiftf  24328  usgrcyclnl1  24332  usgrcyclnl2  24333  3v3e3cycl1  24336  constr3trllem2  24343  4cycl4v4e  24358  4cycl4dv4e  24360  wwlkn0  24381  wlkiswwlk1  24382  wlkiswwlk2lem3  24385  wlklniswwlkn1  24391  usg2wlkeq  24400  wwlknextbi  24417  wwlknredwwlkn0  24419  wwlkextwrd  24420  wwlkextsur  24423  wwlkextprop  24436  clwlkisclwwlklem2a4  24476  clwlkisclwwlklem2a  24477  clwwlkel  24485  clwwlkfo  24489  wwlkext2clwwlk  24495  clwwnisshclwwn  24501  eleclclwwlknlem2  24510  erclwwlkneqlen  24516  erclwwlkntr  24519  hashecclwwlkn1  24526  usghashecclwwlk  24527  clwlkfclwwlk  24536  clwlkfoclwwlk  24537  el2wlkonot  24561  el2spthonot  24562  el2spthonot0  24563  el2wlkonotot0  24564  el2wlkonotot1  24566  usg2spthonot0  24581  vdusgra0nedg  24600  usgravd0nedg  24610  rusgraprop2  24634  clwlknclwlkdifs  24652  eupatrl  24660  1to2vfriswmgra  24698  frgrancvvdeqlem3  24725  frgrancvvdeqlem4  24726  frgrancvvdeqlemB  24731  frgrancvvdeqlemC  24732  usgreghash2spotv  24759  extwwlkfablem1  24767  extwwlkfablem2  24771  numclwwlkun  24772  numclwlk1lem2f1  24787  numclwwlk2lem1  24795  numclwlk2lem2f  24796  ismgm  25014  rngodm1dm2  25112  rngomndo  25115  rngoueqz  25124  zerdivemp1  25128  cdj1i  27044  br8d  27152  sgn3da  28136  br8  28778  br4  28780  sspred  28845  mblfinlem3  29646  mblfinlem4  29647  itg2addnclem  29659  indexdom  29844  zerdivemp1x  29977  pm13.192  30911  iotavalsb  30934  fourierdlem64  31487  nvelim  31688  fveqvfvv  31692  funressnfv  31696  afvpcfv0  31714  afv0nbfvbi  31719  fnbrafvb  31722  tz6.12-afv  31741  afvco2  31744  ndmaovg  31752  f1dmvrnfibi  31795  f1vrnfibi  31796  fzoopth  31823  lswn0  31826  usgra2pth  31837  usgvincvad  31887  usgvincvadALT  31890  usgfis  31929  usgfisALT  31933  iopmapxp  31948  ztprmneprm  32020  lmod0rng  32049  lincext3  32147  zlmodzxznm  32188  bj-snsetex  33611  bj-snglc  33617  opcon3b  34002  ps-1  34282  3atlem5  34292  4atex  34881
  Copyright terms: Public domain W3C validator