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

Theorem 3eqtr3g 2493
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 2484 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr3g.3 . 2  |-  B  =  D
53, 4syl6eq 2486 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-cleq 2421
This theorem is referenced by:  csbnest1g  3824  disjdif2  3880  tppreqb  4144  xpid11  5076  cores2  5368  funcoeqres  5861  fvunsn  6111  caovmo  6520  dftpos2  6998  fvmpt2curryd  7026  tfrlem16  7119  oev2  7233  domss2  7737  enp1ilem  7811  fipreima  7886  dfac5lem3  8554  fpwwe2lem13  9066  canthwelem  9074  canthp1lem2  9077  reclem3pr  9473  mulcmpblnrlem  9493  1idsr  9521  mulgt0sr  9528  mul02lem2  9809  ine0  10053  s1nz  12732  lo1eq  13610  rlimeq  13611  sumeq2ii  13737  fsumf1o  13767  sumss  13768  fsumss  13769  fsumadd  13783  fsumcom2  13813  fsum0diag2  13822  fsummulc2  13823  fsumrelem  13845  isumshft  13875  mertenslem1  13918  prodeq2ii  13945  fprodf1o  13978  prodss  13979  fprodss  13980  fprodmul  13992  fproddiv  13993  fprodcom2  14016  fprodefsum  14127  bitsinv1  14390  bitsinvp1  14397  4sqlem10  14854  setsnid  15128  topnpropd  15294  xpsff1o  15425  homfeqbas  15552  comfffval2  15557  comfeq  15562  oppchomfpropd  15582  isssc  15676  funcpropd  15756  hofpropd  16103  eqglact  16819  lsmmod2  17261  vrgpinv  17354  frgpnabllem1  17444  frgpnabllem2  17445  gsum2dlem2  17538  dprddisj2  17607  ablfac1eulem  17640  ringpropd  17747  crngpropd  17748  mulgass3  17800  rngidpropd  17858  invrpropd  17861  isrhm2d  17891  subrgpropd  17977  rhmpropd  17978  lss0v  18174  lidlrsppropd  18389  ressmpladd  18616  ressmplmul  18617  ressmplvsca  18618  eqcoe1ply1eq  18826  resstopn  20133  lecldbas  20166  isref  20455  txhaus  20593  qustgplem  21066  tuslem  21213  imasdsf1olem  21319  metustsym  21501  reconnlem1  21755  voliunlem1  22380  ismbf3d  22487  i1fima  22513  i1fd  22516  itgfsum  22661  dvmptc  22789  dvmptfsum  22804  dvfsumle  22850  dvfsumlem2  22856  itgsubst  22878  atantayl2  23729  chtdif  23948  ppidif  23953  pythi  26336  hvsubeq0i  26551  hvaddcani  26553  cmcmlem  27079  pj11i  27199  hosubeq0i  27314  riesz3i  27550  pjclem1  27683  pjclem3  27685  st0  27737  chirredi  27882  mdsymi  27899  difeq  27987  subrgchr  28396  locfinref  28507  esumpfinvallem  28734  esum2dlem  28752  carsgclctun  28982  ballotlemgun  29183  cvmliftmolem1  29792  cvmlift3lem6  29835  msubff1  29982  isfne  30780  isfne4  30781  isfne4b  30782  bj-1uplth  31350  bj-2uplth  31364  ptrest  31642  poimirlem3  31646  poimirlem4  31647  poimirlem8  31651  poimirlem15  31658  mblfinlem2  31681  voliunnfl  31687  cdlemg47  34011  ltrnco4  34014  eldioph2  35312  binomcxplemdvbinom  36338  binomcxplemnotnn0  36341  rnfdmpr  38384
  Copyright terms: Public domain W3C validator