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

Theorem 3eqtr3g 2467
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 2458 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr3g.3 . 2  |-  B  =  D
53, 4syl6eq 2460 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  csbnest1g  3271  tppreqb  3907  xpid11  5058  cores2  5349  funcoeqres  5673  fvunsn  5892  caovmo  6251  dftpos2  6463  tfrlem16  6621  oev2  6734  domss2  7233  enp1ilem  7309  fipreima  7378  dfac5lem3  7970  fpwwe2lem13  8481  canthwelem  8489  canthp1lem2  8492  reclem3pr  8890  mulcmpblnrlem  8912  1idsr  8937  mulgt0sr  8944  mul02lem2  9207  ine0  9433  s1nz  11722  lo1eq  12325  rlimeq  12326  sumeq2ii  12450  fsumf1o  12480  sumss  12481  fsumss  12482  fsumadd  12495  fsumcom2  12521  fsum0diag2  12529  fsummulc2  12530  fsumrelem  12549  isumshft  12582  mertenslem1  12624  bitsinv1  12917  bitsinvp1  12924  4sqlem10  13278  setsnid  13472  topnpropd  13627  xpsff1o  13756  homfeqbas  13885  comfffval2  13890  comfeq  13895  oppchomfpropd  13915  isssc  13983  funcpropd  14060  hofpropd  14327  eqglact  14954  lsmmod2  15271  vrgpinv  15364  frgpnabllem1  15447  frgpnabllem2  15448  gsum2d  15509  dprddisj2  15560  ablfac1eulem  15593  rngpropd  15658  crngpropd  15659  mulgass3  15705  rngidpropd  15763  invrpropd  15766  isrhm2d  15792  subrgpropd  15865  rhmpropd  15866  lss0v  16055  lidlrsppropd  16264  ressmpladd  16483  ressmplmul  16484  ressmplvsca  16485  resstopn  17212  lecldbas  17245  ptbasfi  17574  txhaus  17640  divstgplem  18111  tuslem  18258  imasdsf1olem  18364  metustsymOLD  18552  metustsym  18553  reconnlem1  18818  voliunlem1  19405  ismbf3d  19507  i1fima  19531  i1fd  19534  itgfsum  19679  dvmptc  19805  dvmptfsum  19820  dvfsumle  19866  dvfsumlem2  19872  itgsubst  19894  atantayl2  20739  chtdif  20902  ppidif  20907  pythi  22312  hvsubeq0i  22526  hvaddcani  22528  cmcmlem  23054  pj11i  23174  hosubeq0i  23290  riesz3i  23526  pjclem1  23659  pjclem3  23661  st0  23713  chirredi  23858  mdsymi  23875  difeq  23959  subrgchr  24191  esumpfinvallem  24425  ballotlemgun  24743  cvmliftmolem1  24929  cvmlift3lem6  24972  prodeq2ii  25200  fprodf1o  25233  prodss  25234  fprodss  25235  fprodmul  25245  fproddiv  25246  fprodefsum  25259  fprodcom2  25269  mblfinlem  26151  voliunnfl  26157  isfne  26246  isfne4  26247  isfne4b  26248  isref  26257  eldioph2  26718  rnfdmpr  27972  cdlemg47  31230  ltrnco4  31233
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 2393
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2405
  Copyright terms: Public domain W3C validator