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

Theorem 3eqtr3g 2662
Description: A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
Hypotheses
Ref Expression
3eqtr3g.1 (𝜑𝐴 = 𝐵)
3eqtr3g.2 𝐴 = 𝐶
3eqtr3g.3 𝐵 = 𝐷
Assertion
Ref Expression
3eqtr3g (𝜑𝐶 = 𝐷)

Proof of Theorem 3eqtr3g
StepHypRef Expression
1 3eqtr3g.2 . . 3 𝐴 = 𝐶
2 3eqtr3g.1 . . 3 (𝜑𝐴 = 𝐵)
31, 2syl5eqr 2653 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr3g.3 . 2 𝐵 = 𝐷
53, 4syl6eq 2655 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-cleq 2598
This theorem is referenced by:  csbnest1g  3948  disjdif2  3994  diftpsn3  4268  tppreqb  4272  xpid11  5251  cores2  5547  funcoeqres  6061  fvunsn  6324  caovmo  6742  dftpos2  7229  fvmpt2curryd  7257  tfrlem16  7349  oev2  7463  domss2  7977  enp1ilem  8052  fipreima  8128  dfac5lem3  8804  fpwwe2lem13  9316  canthwelem  9324  canthp1lem2  9327  reclem3pr  9723  mulcmpblnrlem  9743  1idsr  9771  mulgt0sr  9778  mul02lem2  10060  ine0  10312  s1nzOLD  13182  lo1eq  14089  rlimeq  14090  sumeq2ii  14213  fsumf1o  14243  sumss  14244  fsumss  14245  fsumadd  14259  fsumcom2  14289  fsumcom2OLD  14290  fsum0diag2  14299  fsummulc2  14300  fsumrelem  14322  isumshft  14352  mertenslem1  14397  prodeq2ii  14424  fprodf1o  14457  prodss  14458  fprodss  14459  fprodmul  14471  fproddiv  14472  fprodcom2  14495  fprodcom2OLD  14496  fprodmodd  14509  fprodefsum  14606  bitsinv1  14944  bitsinvp1  14951  4sqlem10  15431  setsnid  15685  topnpropd  15862  xpsff1o  15993  homfeqbas  16121  comfffval2  16126  comfeq  16131  oppchomfpropd  16151  isssc  16245  funcpropd  16325  hofpropd  16672  eqglact  17410  lsmmod2  17854  vrgpinv  17947  frgpnabllem1  18041  frgpnabllem2  18042  gsum2dlem2  18135  dprddisj2  18203  ablfac1eulem  18236  ringpropd  18347  crngpropd  18348  mulgass3  18402  rngidpropd  18460  invrpropd  18463  isrhm2d  18493  subrgpropd  18579  rhmpropd  18580  lss0v  18779  lidlrsppropd  18993  ressmpladd  19220  ressmplmul  19221  ressmplvsca  19222  eqcoe1ply1eq  19430  resstopn  20738  lecldbas  20771  isref  21060  txhaus  21198  qustgplem  21672  tuslem  21819  imasdsf1olem  21925  metustsym  22107  reconnlem1  22365  voliunlem1  23038  ismbf3d  23140  i1fima  23164  i1fd  23167  itgfsum  23312  dvmptc  23440  dvmptfsum  23455  dvfsumle  23501  dvfsumlem2  23507  itgsubst  23529  atantayl2  24378  chtdif  24597  ppidif  24602  pythi  26891  hvsubeq0i  27106  hvaddcani  27108  cmcmlem  27636  pj11i  27756  hosubeq0i  27871  riesz3i  28107  pjclem1  28240  pjclem3  28242  st0  28294  chirredi  28439  mdsymi  28456  difeq  28541  subrgchr  28927  locfinref  29038  esumpfinvallem  29265  esum2dlem  29283  carsgclctun  29512  ballotlemgun  29715  cvmliftmolem1  30319  cvmlift3lem6  30362  msubff1  30509  isfne  31306  isfne4  31307  isfne4b  31308  bj-1uplth  31987  bj-2uplth  32001  matunitlindflem1  32374  ptrest  32377  poimirlem3  32381  poimirlem4  32382  poimirlem8  32386  poimirlem15  32393  mblfinlem2  32416  voliunnfl  32422  cdlemg47  34841  ltrnco4  34844  eldioph2  36142  binomcxplemdvbinom  37373  binomcxplemnotnn0  37376  rnfdmpr  40137
  Copyright terms: Public domain W3C validator