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

Theorem 3eqtr3g 2518
Description: A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
Hypotheses
Ref Expression
3eqtr3g.1  |-  ( ph  ->  A  =  B )
3eqtr3g.2  |-  A  =  C
3eqtr3g.3  |-  B  =  D
Assertion
Ref Expression
3eqtr3g  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr3g
StepHypRef Expression
1 3eqtr3g.2 . . 3  |-  A  =  C
2 3eqtr3g.1 . . 3  |-  ( ph  ->  A  =  B )
31, 2syl5eqr 2509 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr3g.3 . 2  |-  B  =  D
53, 4syl6eq 2511 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446
This theorem is referenced by:  csbnest1g  3808  tppreqb  4125  xpid11  5172  cores2  5461  funcoeqres  5782  fvunsn  6022  caovmo  6413  dftpos2  6875  fvmpt2curryd  6903  tfrlem16  6965  oev2  7076  domss2  7583  enp1ilem  7660  fipreima  7731  dfac5lem3  8409  fpwwe2lem13  8923  canthwelem  8931  canthp1lem2  8934  reclem3pr  9332  mulcmpblnrlem  9354  1idsr  9379  mulgt0sr  9386  mul02lem2  9660  ine0  9894  s1nz  12418  lo1eq  13167  rlimeq  13168  sumeq2ii  13291  fsumf1o  13321  sumss  13322  fsumss  13323  fsumadd  13336  fsumcom2  13362  fsum0diag2  13371  fsummulc2  13372  fsumrelem  13391  isumshft  13423  mertenslem1  13465  bitsinv1  13759  bitsinvp1  13766  4sqlem10  14129  setsnid  14337  topnpropd  14497  xpsff1o  14628  homfeqbas  14757  comfffval2  14762  comfeq  14767  oppchomfpropd  14787  isssc  14855  funcpropd  14932  hofpropd  15199  eqglact  15854  lsmmod2  16297  vrgpinv  16390  frgpnabllem1  16475  frgpnabllem2  16476  gsum2dlem2  16587  gsum2dOLD  16589  dprddisj2  16662  dprddisj2OLD  16663  ablfac1eulem  16698  rngpropd  16802  crngpropd  16803  mulgass3  16855  rngidpropd  16913  invrpropd  16916  isrhm2d  16944  subrgpropd  17025  rhmpropd  17026  lss0v  17223  lidlrsppropd  17438  ressmpladd  17663  ressmplmul  17664  ressmplvsca  17665  resstopn  18925  lecldbas  18958  ptbasfi  19289  txhaus  19355  divstgplem  19826  tuslem  19977  imasdsf1olem  20083  metustsymOLD  20271  metustsym  20272  reconnlem1  20538  voliunlem1  21167  ismbf3d  21268  i1fima  21292  i1fd  21295  itgfsum  21440  dvmptc  21568  dvmptfsum  21583  dvfsumle  21629  dvfsumlem2  21635  itgsubst  21657  atantayl2  22469  chtdif  22632  ppidif  22637  pythi  24422  hvsubeq0i  24637  hvaddcani  24639  cmcmlem  25166  pj11i  25286  hosubeq0i  25402  riesz3i  25638  pjclem1  25771  pjclem3  25773  st0  25825  chirredi  25970  mdsymi  25987  difeq  26071  subrgchr  26427  esumpfinvallem  26688  ballotlemgun  27071  cvmliftmolem1  27334  cvmlift3lem6  27377  prodeq2ii  27590  fprodf1o  27623  prodss  27624  fprodss  27625  fprodmul  27635  fproddiv  27636  fprodefsum  27649  fprodcom2  27659  ptrest  28593  mblfinlem2  28597  voliunnfl  28603  isfne  28708  isfne4  28709  isfne4b  28710  isref  28719  eldioph2  29268  rnfdmpr  30317  eqcoe1ply1eq  31008  bj-disjdif  32798  bj-1uplth  32852  bj-2uplth  32866  cdlemg47  34738  ltrnco4  34741
  Copyright terms: Public domain W3C validator