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

Theorem 3eqtr3g 2459
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 2450 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr3g.3 . 2  |-  B  =  D
53, 4syl6eq 2452 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  csbnest1g  3263  tppreqb  3899  xpid11  5050  cores2  5341  funcoeqres  5665  fvunsn  5884  caovmo  6243  dftpos2  6455  tfrlem16  6613  oev2  6726  domss2  7225  enp1ilem  7301  fipreima  7370  dfac5lem3  7962  fpwwe2lem13  8473  canthwelem  8481  canthp1lem2  8484  reclem3pr  8882  mulcmpblnrlem  8904  1idsr  8929  mulgt0sr  8936  mul02lem2  9199  ine0  9425  s1nz  11714  lo1eq  12317  rlimeq  12318  sumeq2ii  12442  fsumf1o  12472  sumss  12473  fsumss  12474  fsumadd  12487  fsumcom2  12513  fsum0diag2  12521  fsummulc2  12522  fsumrelem  12541  isumshft  12574  mertenslem1  12616  bitsinv1  12909  bitsinvp1  12916  4sqlem10  13270  setsnid  13464  topnpropd  13619  xpsff1o  13748  homfeqbas  13877  comfffval2  13882  comfeq  13887  oppchomfpropd  13907  isssc  13975  funcpropd  14052  hofpropd  14319  eqglact  14946  lsmmod2  15263  vrgpinv  15356  frgpnabllem1  15439  frgpnabllem2  15440  gsum2d  15501  dprddisj2  15552  ablfac1eulem  15585  rngpropd  15650  crngpropd  15651  mulgass3  15697  rngidpropd  15755  invrpropd  15758  isrhm2d  15784  subrgpropd  15857  rhmpropd  15858  lss0v  16047  lidlrsppropd  16256  ressmpladd  16475  ressmplmul  16476  ressmplvsca  16477  resstopn  17204  lecldbas  17237  ptbasfi  17566  txhaus  17632  divstgplem  18103  tuslem  18250  imasdsf1olem  18356  metustsymOLD  18544  metustsym  18545  reconnlem1  18810  voliunlem1  19397  ismbf3d  19499  i1fima  19523  i1fd  19526  itgfsum  19671  dvmptc  19797  dvmptfsum  19812  dvfsumle  19858  dvfsumlem2  19864  itgsubst  19886  atantayl2  20731  chtdif  20894  ppidif  20899  pythi  22304  hvsubeq0i  22518  hvaddcani  22520  cmcmlem  23046  pj11i  23166  hosubeq0i  23282  riesz3i  23518  pjclem1  23651  pjclem3  23653  st0  23705  chirredi  23850  mdsymi  23867  difeq  23951  subrgchr  24183  esumpfinvallem  24417  ballotlemgun  24735  cvmliftmolem1  24921  cvmlift3lem6  24964  prodeq2ii  25192  fprodf1o  25225  prodss  25226  fprodss  25227  fprodmul  25237  fproddiv  25238  fprodefsum  25251  fprodcom2  25261  mblfinlem  26143  voliunnfl  26149  isfne  26238  isfne4  26239  isfne4b  26240  isref  26249  eldioph2  26710  rnfdmpr  27964  cdlemg47  31218  ltrnco4  31221
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator