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

Theorem 3eqtr3g 2421
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 2412 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr3g.3 . 2  |-  B  =  D
53, 4syl6eq 2414 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1647
This theorem is referenced by:  csbnest1g  3219  tppreqb  3854  xpid11  5003  cores2  5288  funcoeqres  5610  fvunsn  5825  caovmo  6184  dftpos2  6393  tfrlem16  6551  oev2  6664  domss2  7163  enp1ilem  7239  fipreima  7308  dfac5lem3  7899  fpwwe2lem13  8411  canthwelem  8419  canthp1lem2  8422  reclem3pr  8820  mulcmpblnrlem  8842  1idsr  8867  mulgt0sr  8874  mul02lem2  9136  ine0  9362  s1nz  11646  lo1eq  12249  rlimeq  12250  sumeq2ii  12374  fsumf1o  12404  sumss  12405  fsumss  12406  fsumadd  12419  fsumcom2  12445  fsum0diag2  12453  fsummulc2  12454  fsumrelem  12473  isumshft  12506  mertenslem1  12548  bitsinvp1  12848  4sqlem10  13202  setsnid  13396  topnpropd  13551  xpsff1o  13680  homfeqbas  13809  comfffval2  13814  comfeq  13819  oppchomfpropd  13839  isssc  13907  funcpropd  13984  hofpropd  14251  eqglact  14878  lsmmod2  15195  vrgpinv  15288  frgpnabllem1  15371  frgpnabllem2  15372  gsum2d  15433  dprddisj2  15484  ablfac1eulem  15517  rngpropd  15582  crngpropd  15583  mulgass3  15629  rngidpropd  15687  invrpropd  15690  isrhm2d  15716  subrgpropd  15789  rhmpropd  15790  lss0v  15983  lidlrsppropd  16192  ressmpladd  16411  ressmplmul  16412  ressmplvsca  16413  resstopn  17133  lecldbas  17166  ptbasfi  17493  txhaus  17558  divstgplem  18016  imasdsf1olem  18150  reconnlem1  18545  voliunlem1  19122  ismbf3d  19224  i1fima  19248  i1fd  19251  itgfsum  19396  dvmptc  19522  dvmptfsum  19537  dvfsumle  19583  dvfsumlem2  19589  itgsubst  19611  atantayl2  20456  chtdif  20619  ppidif  20624  pythi  21862  hvsubeq0i  22076  hvaddcani  22078  cmcmlem  22604  pj11i  22724  hosubeq0i  22840  riesz3i  23076  pjclem1  23209  pjclem3  23211  st0  23263  chirredi  23408  mdsymi  23425  difeq  23516  tuslem  23885  metustsym  23919  esumpfinvallem  24050  ballotlemgun  24351  cvmliftmolem1  24536  cvmlift3lem6  24579  prodeq2ii  24808  fprodf1o  24841  prodss  24842  fprodss  24843  fprodmul  24853  fproddiv  24854  fprodefsum  24867  voliunnfl  25758  isfne  25860  isfne4  25861  isfne4b  25862  isref  25871  eldioph2  26432  cdlemg47  30984  ltrnco4  30987
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-ex 1547  df-cleq 2359
  Copyright terms: Public domain W3C validator