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

Theorem 3eqtr3g 2493
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 2484 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr3g.3 . 2  |-  B  =  D
53, 4syl6eq 2486 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653
This theorem is referenced by:  csbnest1g  3305  tppreqb  3941  xpid11  5094  cores2  5385  funcoeqres  5709  fvunsn  5928  caovmo  6287  dftpos2  6499  tfrlem16  6657  oev2  6770  domss2  7269  enp1ilem  7345  fipreima  7415  dfac5lem3  8011  fpwwe2lem13  8522  canthwelem  8530  canthp1lem2  8533  reclem3pr  8931  mulcmpblnrlem  8953  1idsr  8978  mulgt0sr  8985  mul02lem2  9248  ine0  9474  s1nz  11764  lo1eq  12367  rlimeq  12368  sumeq2ii  12492  fsumf1o  12522  sumss  12523  fsumss  12524  fsumadd  12537  fsumcom2  12563  fsum0diag2  12571  fsummulc2  12572  fsumrelem  12591  isumshft  12624  mertenslem1  12666  bitsinv1  12959  bitsinvp1  12966  4sqlem10  13320  setsnid  13514  topnpropd  13669  xpsff1o  13798  homfeqbas  13927  comfffval2  13932  comfeq  13937  oppchomfpropd  13957  isssc  14025  funcpropd  14102  hofpropd  14369  eqglact  14996  lsmmod2  15313  vrgpinv  15406  frgpnabllem1  15489  frgpnabllem2  15490  gsum2d  15551  dprddisj2  15602  ablfac1eulem  15635  rngpropd  15700  crngpropd  15701  mulgass3  15747  rngidpropd  15805  invrpropd  15808  isrhm2d  15834  subrgpropd  15907  rhmpropd  15908  lss0v  16097  lidlrsppropd  16306  ressmpladd  16525  ressmplmul  16526  ressmplvsca  16527  resstopn  17255  lecldbas  17288  ptbasfi  17618  txhaus  17684  divstgplem  18155  tuslem  18302  imasdsf1olem  18408  metustsymOLD  18596  metustsym  18597  reconnlem1  18862  voliunlem1  19449  ismbf3d  19549  i1fima  19573  i1fd  19576  itgfsum  19721  dvmptc  19849  dvmptfsum  19864  dvfsumle  19910  dvfsumlem2  19916  itgsubst  19938  atantayl2  20783  chtdif  20946  ppidif  20951  pythi  22356  hvsubeq0i  22570  hvaddcani  22572  cmcmlem  23098  pj11i  23218  hosubeq0i  23334  riesz3i  23570  pjclem1  23703  pjclem3  23705  st0  23757  chirredi  23902  mdsymi  23919  difeq  24003  subrgchr  24235  esumpfinvallem  24469  ballotlemgun  24787  cvmliftmolem1  24973  cvmlift3lem6  25016  prodeq2ii  25244  fprodf1o  25277  prodss  25278  fprodss  25279  fprodmul  25289  fproddiv  25290  fprodefsum  25303  fprodcom2  25313  mblfinlem2  26255  voliunnfl  26261  isfne  26361  isfne4  26362  isfne4b  26363  isref  26372  eldioph2  26833  rnfdmpr  28100  cdlemg47  31606  ltrnco4  31609
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431
  Copyright terms: Public domain W3C validator