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

Theorem 3eqtr3g 2678
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 2669 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr3g.3 . 2 𝐵 = 𝐷
53, 4syl6eq 2671 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614
This theorem is referenced by:  csbnest1g  3979  disjdif2  4025  diftpsn3  4308  tppreqb  4312  xpid11  5317  cores2  5617  funcoeqres  6134  fvunsn  6410  caovmo  6836  dftpos2  7329  fvmpt2curryd  7357  tfrlem16  7449  oev2  7563  domss2  8079  enp1ilem  8154  fipreima  8232  dfac5lem3  8908  fpwwe2lem13  9424  canthwelem  9432  canthp1lem2  9435  reclem3pr  9831  mulcmpblnrlem  9851  1idsr  9879  mulgt0sr  9886  mul02lem2  10173  ine0  10425  s1nzOLD  13342  lo1eq  14249  rlimeq  14250  sumeq2ii  14373  fsumf1o  14403  sumss  14404  fsumss  14405  fsumadd  14419  fsumcom2  14452  fsumcom2OLD  14453  fsum0diag2  14462  fsummulc2  14463  fsumrelem  14485  isumshft  14515  mertenslem1  14560  prodeq2ii  14587  fprodf1o  14620  prodss  14621  fprodss  14622  fprodmul  14634  fproddiv  14635  fprodcom2  14658  fprodcom2OLD  14659  fprodmodd  14672  fprodefsum  14769  bitsinv1  15107  bitsinvp1  15114  4sqlem10  15594  setsnid  15855  topnpropd  16037  xpsff1o  16168  homfeqbas  16296  comfffval2  16301  comfeq  16306  oppchomfpropd  16326  isssc  16420  funcpropd  16500  hofpropd  16847  eqglact  17585  lsmmod2  18029  vrgpinv  18122  frgpnabllem1  18216  frgpnabllem2  18217  gsum2dlem2  18310  dprddisj2  18378  ablfac1eulem  18411  ringpropd  18522  crngpropd  18523  mulgass3  18577  rngidpropd  18635  invrpropd  18638  isrhm2d  18668  subrgpropd  18754  rhmpropd  18755  lss0v  18956  lidlrsppropd  19170  ressmpladd  19397  ressmplmul  19398  ressmplvsca  19399  eqcoe1ply1eq  19607  resstopn  20930  lecldbas  20963  isref  21252  txhaus  21390  qustgplem  21864  tuslem  22011  imasdsf1olem  22118  metustsym  22300  reconnlem1  22569  voliunlem1  23258  ismbf3d  23361  i1fima  23385  i1fd  23388  itgfsum  23533  dvmptc  23661  dvmptfsum  23676  dvfsumle  23722  dvfsumlem2  23728  itgsubst  23750  atantayl2  24599  chtdif  24818  ppidif  24823  pythi  27593  hvsubeq0i  27808  hvaddcani  27810  cmcmlem  28338  pj11i  28458  hosubeq0i  28573  riesz3i  28809  pjclem1  28942  pjclem3  28944  st0  28996  chirredi  29141  mdsymi  29158  difeq  29243  subrgchr  29621  locfinref  29732  esumpfinvallem  29959  esum2dlem  29977  carsgclctun  30206  ballotlemgun  30409  cvmliftmolem1  31024  cvmlift3lem6  31067  msubff1  31214  isfne  32029  isfne4  32030  isfne4b  32031  bj-1uplth  32695  bj-2uplth  32709  matunitlindflem1  33076  ptrest  33079  poimirlem3  33083  poimirlem4  33084  poimirlem8  33088  poimirlem15  33095  mblfinlem2  33118  voliunnfl  33124  cdlemg47  35543  ltrnco4  35546  eldioph2  36844  binomcxplemdvbinom  38073  binomcxplemnotnn0  38076  compne  38164  rnfdmpr  40627
  Copyright terms: Public domain W3C validator