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

Theorem 3eqtr3g 2488
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 2479 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr3g.3 . 2  |-  B  =  D
53, 4syl6eq 2481 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426
This theorem is referenced by:  csbnest1g  3685  tppreqb  4002  xpid11  5048  cores2  5338  funcoeqres  5659  fvunsn  5897  caovmo  6289  dftpos2  6751  tfrlem16  6838  oev2  6951  domss2  7458  enp1ilem  7534  fipreima  7605  dfac5lem3  8283  fpwwe2lem13  8797  canthwelem  8805  canthp1lem2  8808  reclem3pr  9206  mulcmpblnrlem  9228  1idsr  9253  mulgt0sr  9260  mul02lem2  9534  ine0  9768  s1nz  12281  lo1eq  13030  rlimeq  13031  sumeq2ii  13154  fsumf1o  13184  sumss  13185  fsumss  13186  fsumadd  13199  fsumcom2  13225  fsum0diag2  13233  fsummulc2  13234  fsumrelem  13253  isumshft  13285  mertenslem1  13327  bitsinv1  13621  bitsinvp1  13628  4sqlem10  13991  setsnid  14199  topnpropd  14358  xpsff1o  14489  homfeqbas  14618  comfffval2  14623  comfeq  14628  oppchomfpropd  14648  isssc  14716  funcpropd  14793  hofpropd  15060  eqglact  15712  lsmmod2  16153  vrgpinv  16246  frgpnabllem1  16331  frgpnabllem2  16332  gsum2dlem2  16436  gsum2dOLD  16438  dprddisj2  16511  dprddisj2OLD  16512  ablfac1eulem  16547  rngpropd  16612  crngpropd  16613  mulgass3  16663  rngidpropd  16721  invrpropd  16724  isrhm2d  16750  subrgpropd  16823  rhmpropd  16824  lss0v  17019  lidlrsppropd  17234  ressmpladd  17470  ressmplmul  17471  ressmplvsca  17472  resstopn  18632  lecldbas  18665  ptbasfi  18996  txhaus  19062  divstgplem  19533  tuslem  19684  imasdsf1olem  19790  metustsymOLD  19978  metustsym  19979  reconnlem1  20245  voliunlem1  20873  ismbf3d  20974  i1fima  20998  i1fd  21001  itgfsum  21146  dvmptc  21274  dvmptfsum  21289  dvfsumle  21335  dvfsumlem2  21341  itgsubst  21363  atantayl2  22218  chtdif  22381  ppidif  22386  pythi  24073  hvsubeq0i  24288  hvaddcani  24290  cmcmlem  24817  pj11i  24937  hosubeq0i  25053  riesz3i  25289  pjclem1  25422  pjclem3  25424  st0  25476  chirredi  25621  mdsymi  25638  difeq  25723  subrgchr  26115  esumpfinvallem  26377  ballotlemgun  26755  cvmliftmolem1  27018  cvmlift3lem6  27061  prodeq2ii  27273  fprodf1o  27306  prodss  27307  fprodss  27308  fprodmul  27318  fproddiv  27319  fprodefsum  27332  fprodcom2  27342  ptrest  28269  mblfinlem2  28273  voliunnfl  28279  isfne  28384  isfne4  28385  isfne4b  28386  isref  28395  eldioph2  28945  rnfdmpr  29995  bj-disjdif  32029  bj-1uplth  32083  bj-2uplth  32097  cdlemg47  33953  ltrnco4  33956
  Copyright terms: Public domain W3C validator