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

Theorem 3eqtr3g 2444
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 2435 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr3g.3 . 2  |-  B  =  D
53, 4syl6eq 2437 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  csbnest1g  3248  tppreqb  3884  xpid11  5033  cores2  5324  funcoeqres  5648  fvunsn  5866  caovmo  6225  dftpos2  6434  tfrlem16  6592  oev2  6705  domss2  7204  enp1ilem  7280  fipreima  7349  dfac5lem3  7941  fpwwe2lem13  8452  canthwelem  8460  canthp1lem2  8463  reclem3pr  8861  mulcmpblnrlem  8883  1idsr  8908  mulgt0sr  8915  mul02lem2  9177  ine0  9403  s1nz  11688  lo1eq  12291  rlimeq  12292  sumeq2ii  12416  fsumf1o  12446  sumss  12447  fsumss  12448  fsumadd  12461  fsumcom2  12487  fsum0diag2  12495  fsummulc2  12496  fsumrelem  12515  isumshft  12548  mertenslem1  12590  bitsinv1  12883  bitsinvp1  12890  4sqlem10  13244  setsnid  13438  topnpropd  13593  xpsff1o  13722  homfeqbas  13851  comfffval2  13856  comfeq  13861  oppchomfpropd  13881  isssc  13949  funcpropd  14026  hofpropd  14293  eqglact  14920  lsmmod2  15237  vrgpinv  15330  frgpnabllem1  15413  frgpnabllem2  15414  gsum2d  15475  dprddisj2  15526  ablfac1eulem  15559  rngpropd  15624  crngpropd  15625  mulgass3  15671  rngidpropd  15729  invrpropd  15732  isrhm2d  15758  subrgpropd  15831  rhmpropd  15832  lss0v  16021  lidlrsppropd  16230  ressmpladd  16449  ressmplmul  16450  ressmplvsca  16451  resstopn  17174  lecldbas  17207  ptbasfi  17536  txhaus  17602  divstgplem  18073  tuslem  18220  imasdsf1olem  18313  metustsym  18477  reconnlem1  18730  voliunlem1  19313  ismbf3d  19415  i1fima  19439  i1fd  19442  itgfsum  19587  dvmptc  19713  dvmptfsum  19728  dvfsumle  19774  dvfsumlem2  19780  itgsubst  19802  atantayl2  20647  chtdif  20810  ppidif  20815  pythi  22201  hvsubeq0i  22415  hvaddcani  22417  cmcmlem  22943  pj11i  23063  hosubeq0i  23179  riesz3i  23415  pjclem1  23548  pjclem3  23550  st0  23602  chirredi  23747  mdsymi  23764  difeq  23844  esumpfinvallem  24262  ballotlemgun  24563  cvmliftmolem1  24749  cvmlift3lem6  24792  prodeq2ii  25020  fprodf1o  25053  prodss  25054  fprodss  25055  fprodmul  25065  fproddiv  25066  fprodefsum  25079  voliunnfl  25957  isfne  26041  isfne4  26042  isfne4b  26043  isref  26052  eldioph2  26513  cdlemg47  30852  ltrnco4  30855
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 1661  ax-8 1682  ax-11 1753  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2382
  Copyright terms: Public domain W3C validator