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

Theorem 3eqtr3g 2508
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 2499 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr3g.3 . 2  |-  B  =  D
53, 4syl6eq 2501 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-cleq 2444
This theorem is referenced by:  csbnest1g  3790  disjdif2  3846  tppreqb  4113  xpid11  5056  cores2  5348  funcoeqres  5844  fvunsn  6096  caovmo  6506  dftpos2  6990  fvmpt2curryd  7018  tfrlem16  7111  oev2  7225  domss2  7731  enp1ilem  7805  fipreima  7880  dfac5lem3  8556  fpwwe2lem13  9067  canthwelem  9075  canthp1lem2  9078  reclem3pr  9474  mulcmpblnrlem  9494  1idsr  9522  mulgt0sr  9529  mul02lem2  9810  ine0  10054  s1nz  12745  lo1eq  13632  rlimeq  13633  sumeq2ii  13759  fsumf1o  13789  sumss  13790  fsumss  13791  fsumadd  13805  fsumcom2  13835  fsum0diag2  13844  fsummulc2  13845  fsumrelem  13867  isumshft  13897  mertenslem1  13940  prodeq2ii  13967  fprodf1o  14000  prodss  14001  fprodss  14002  fprodmul  14014  fproddiv  14015  fprodcom2  14038  fprodefsum  14149  bitsinv1  14416  bitsinvp1  14423  4sqlem10  14891  setsnid  15165  topnpropd  15335  xpsff1o  15474  homfeqbas  15601  comfffval2  15606  comfeq  15611  oppchomfpropd  15631  isssc  15725  funcpropd  15805  hofpropd  16152  eqglact  16868  lsmmod2  17326  vrgpinv  17419  frgpnabllem1  17509  frgpnabllem2  17510  gsum2dlem2  17603  dprddisj2  17672  ablfac1eulem  17705  ringpropd  17812  crngpropd  17813  mulgass3  17865  rngidpropd  17923  invrpropd  17926  isrhm2d  17956  subrgpropd  18042  rhmpropd  18043  lss0v  18239  lidlrsppropd  18454  ressmpladd  18681  ressmplmul  18682  ressmplvsca  18683  eqcoe1ply1eq  18891  resstopn  20202  lecldbas  20235  isref  20524  txhaus  20662  qustgplem  21135  tuslem  21282  imasdsf1olem  21388  metustsym  21570  reconnlem1  21844  voliunlem1  22503  ismbf3d  22610  i1fima  22636  i1fd  22639  itgfsum  22784  dvmptc  22912  dvmptfsum  22927  dvfsumle  22973  dvfsumlem2  22979  itgsubst  23001  atantayl2  23864  chtdif  24085  ppidif  24090  pythi  26491  hvsubeq0i  26716  hvaddcani  26718  cmcmlem  27244  pj11i  27364  hosubeq0i  27479  riesz3i  27715  pjclem1  27848  pjclem3  27850  st0  27902  chirredi  28047  mdsymi  28064  difeq  28151  subrgchr  28557  locfinref  28668  esumpfinvallem  28895  esum2dlem  28913  carsgclctun  29153  ballotlemgun  29357  ballotlemgunOLD  29395  cvmliftmolem1  30004  cvmlift3lem6  30047  msubff1  30194  isfne  30995  isfne4  30996  isfne4b  30997  bj-1uplth  31601  bj-2uplth  31615  ptrest  31939  poimirlem3  31943  poimirlem4  31944  poimirlem8  31948  poimirlem15  31955  mblfinlem2  31978  voliunnfl  31984  cdlemg47  34303  ltrnco4  34306  eldioph2  35604  binomcxplemdvbinom  36702  binomcxplemnotnn0  36705  rnfdmpr  39015
  Copyright terms: Public domain W3C validator