Theorem 3eqtr4g 2468

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
3eqtr4g.1	|- ( ph -> A = B )
3eqtr4g.2	|- C = A
3eqtr4g.3	|- D = B

Assertion

Ref	Expression
3eqtr4g	|- ( ph -> C = D )

Proof of Theorem 3eqtr4g

Step	Hyp	Ref	Expression
1		3eqtr4g.2	. . 3 |- C = A
2		3eqtr4g.1	. . 3 |- ( ph -> A = B )
3	1, 2	syl5eq 2455	. 2 |- ( ph -> C = B )
4		3eqtr4g.3	. 2 |- D = B
5	3, 4	syl6eqr 2461	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-cleq 2394

This theorem is referenced by:  rabbidva2  3049  rabeqf  3052  csbeq1  3376  csbeq2  3377  difeq1  3554  difeq2  3555  uneq2  3591  ineq2  3635  symdifeq1  3672  symdifeq2  3673  dfrab3ss  3728  csbeq2d  3785  csbnestgf  3790  ifeq1  3889  ifeq2  3890  pweq  3958  sneq  3982  csbsng  4030  csbprg  4031  rabsn  4039  preq1  4051  preq2  4052  tpeq1  4060  tpeq2  4061  tpeq3  4062  prprc1  4082  opeq1  4159  opeq2  4160  oteq1  4168  oteq2  4169  oteq3  4170  unieq  4199  csbuni  4219  inteq  4230  iineq1  4286  iineq2  4289  dfiin2g  4304  iinrab  4333  iinin1  4342  iinxprg  4352  iununi  4359  opabbid  4457  mpteq12f  4471  csbmpt12  4724  xpeq1  4837  xpeq2  4838  rneq  5049  reseq1  5088  reseq2  5089  resmpt  5143  imaeq1  5152  imaeq2  5153  mptcnv  5226  dmpropg  5297  rnpropg  5304  cores  5326  cores2  5336  xpco  5364  predeq123  5368  suceq  5475  iotaeq  5541  iotabi  5542  fntpg  5624  imain  5645  f1oprswap  5838  fveq1  5848  fveq2  5849  fvres  5863  csbfv12  5884  fnimapr  5913  fvco2  5924  residpr  6055  fsnunfv  6091  fsnunres  6092  funiunfv  6141  fliftf  6196  isoini2  6218  riotaeqdv  6241  riotabidv  6242  riotauni  6246  riotabidva  6256  snriota  6269  oveq  6284  oveq1  6285  oveq2  6286  oprabbid  6331  mpt2eq123  6337  mpt2eq123dva  6339  mpt2eq3dva  6342  resmpt2  6381  ovres  6423  f1ocnvd  6505  ofeq  6523  ofreq  6524  fpar  6888  wrecseq123  7014  onovuni  7046  recseq  7077  tfr2a  7098  rdgeq1  7114  rdgeq2  7115  rdgsucmptf  7131  frsucmpt  7140  seqomeq12  7156  seqomsuc  7159  omopthi  7343  eceq1  7384  eceq2  7386  qseq1  7398  qseq2  7399  uniqs  7408  ecinxp  7423  qsinxp  7424  erovlem  7444  ecopovtrn  7451  ixpeq1  7518  supeq1  7938  supeq2  7941  supeq3  7942  supeq123d  7943  oieq1  7971  oieq2  7972  ordtypelem1  7977  inf3lemc  8076  wemapwe  8171  wemapweOLD  8172  r1sucg  8219  r1limg  8221  rankprb  8301  karden  8345  cardiun  8395  acneq  8456  alephlim  8480  alephsuc  8481  alephfplem2  8518  infpssrlem2  8716  fin23lem34  8758  fin23lem35  8759  zorn2lem1  8908  zorn2lem7  8914  fpwwe2lem6  9043  fpwwe2lem13  9050  addpiord  9292  mulpiord  9293  addpqnq  9346  mulpqnq  9349  addassnq  9366  mulassnq  9367  distrnq  9369  lterpq  9378  ltexnq  9383  ltsrpr  9484  00sr  9506  recexsrlem  9510  mulgt0sr  9512  addcnsrec  9550  mulcnsrec  9551  negeq  9848  csbnegg  9853  negsubdi  9911  mulneg1  10034  deceq1  11022  deceq2  11023  xnegeq  11459  fseq1p1m1  11807  om2uzrdg  12108  uzrdgsuci  12112  seqeq1  12154  seqeq2  12155  seqeq3  12156  seqfeq4  12200  seqof  12208  hashprg  12509  hashmap  12542  hashtpg  12572  csbwrdg  12623  s1eq  12666  cats1co  12877  s2eqd  12883  s3eqd  12884  s4eqd  12885  s5eqd  12886  s6eqd  12887  s7eqd  12888  s8eqd  12889  xpcogend  12957  shftval  13056  limsupgle  13449  lo1eq  13540  rlimeq  13541  sumeq1  13660  sumeq2w  13663  sumeq2ii  13664  zsum  13689  sumss2  13697  fsumsplitsnun  13721  isumclim3  13725  fsumcom2  13740  incexclem  13799  incexc2  13801  isumshft  13802  prodeq1f  13867  prodeq2w  13871  prodeq2ii  13872  zprod  13896  fprodm1s  13926  fprodp1s  13927  fprodcom2  13940  iprodclim3  13945  ef0lem  14023  ruclem7  14178  sadcp1  14314  smupp1  14339  smueqlem  14349  algrp1  14412  dfphi2  14513  prmdiveq  14525  pceulem  14578  vdwlem6  14713  cshwsiun  14793  setsid  14884  elbasfv  14890  elbasov  14891  imastset  15136  imasvscaval  15152  xpscg  15172  isoval  15378  funcoppc  15488  fulloppc  15535  fuccofval  15572  natpropd  15589  catccofval  15703  xpchomfval  15772  xpccofval  15775  lubfval  15932  glbfval  15945  grpidpropd  16212  gsumpropd2lem  16224  frmdplusg  16346  grpinvpropd  16437  grpsubpropd  16464  grpsubpropd2  16465  mulgpropd  16499  oppgmnd  16713  symgplusg  16738  sylow1lem2  16943  sylow3lem1  16971  prds1  17583  pwsmgp  17587  opprring  17600  rngidpropd  17664  dvdsrpropd  17665  unitpropd  17666  invrpropd  17667  rhm1  17699  lmhmpropd  18039  lidlrsppropd  18198  lpival  18213  rrgsuppOLD  18260  ressascl  18313  asclpropd  18315  aspval2  18316  psrbas  18350  psrbasOLD  18351  psrplusg  18354  psrmulr  18357  psrvscafval  18363  resspsrbas  18390  ressmplbas2  18437  opsrle  18460  opsrbaslem  18462  vr1val  18551  ressply1add  18591  ressply1mul  18592  ressply1vsca  18593  psrplusgpropd  18597  mplbaspropd  18598  psropprmul  18599  ply1baspropd  18604  ply1plusgpropd  18605  ply1sca2  18615  subrgvr1  18622  coe1mul2lem2  18629  ply1coe1eq  18660  zrhpropd  18852  znle  18873  frlmplusgval  19093  frlmvscafval  19095  mamudi  19197  mamudir  19198  matrcl  19206  oftpos  19246  mattpos1  19250  mdetfval  19380  mdetrlin  19396  mdetrsca  19397  mdetrsca2  19398  mdetrlin2  19401  mdetunilem5  19410  madufval  19431  madugsum  19437  idmatidpmat  19530  cpmidpmat  19666  cncmp  20185  2ndcsep  20252  llyeq  20263  nllyeq  20264  xkouni  20392  hmphindis  20590  xkocnv  20607  ptcmplem2  20845  snclseqg  20906  prdstmdd  20914  ustexsym  21010  ucnextcn  21099  metreslem  21157  comet  21308  nrmmetd  21387  nmpropd  21406  isngp3  21410  ngpds  21415  subgnm  21439  tngnm  21457  idnghm  21542  cnmetdval  21570  cnmpt2pc  21720  htpyco2  21771  phtpyco2  21782  clsocv  21982  rrxprds  22113  rrxnm  22115  ovolunlem1a  22199  voliunlem3  22254  ioombl1lem4  22263  uniioombllem4  22287  itg11  22390  itgeq1f  22470  itgeq2  22476  iblss2  22504  itgss  22510  itgeqa  22512  itgfsum  22525  itgsplit  22534  ditgeq1  22544  ditgeq2  22545  ditgeq3  22546  dvcmulf  22640  dvmptfsum  22668  dvcnvrelem2  22711  mdegfval  22752  mdegpropd  22776  deg1propd  22778  plyeq0  22900  coe11  22942  dgrlt  22955  dgradd2  22957  dgrmulc  22960  dvply1  22972  fta1lem  22995  pserulm  23109  rlimcnp2  23622  jensenlem1  23642  basellem5  23739  dchrbas  23891  dchrrcl  23896  dchrplusg  23903  dchrfi  23911  lgsdi  23988  lgseisenlem2  24006  lgsquadlem3  24012  dchrmusumlema  24059  rpvmasum2  24078  dchrisum0lema  24080  pntlemg  24164  colperpexlem2  24491  axlowdimlem13  24674  nbgraf1olem5  24862  nb3graprlem1  24868  constr2spthlem1  25013  constr3pthlem1  25072  constr3pthlem2  25073  avril1  25588  0vfval  25913  imsval  26005  imsdval  26006  bcseqi  26451  normpythi  26473  cm0  26941  fh1  26950  pjcji  27016  opsqrlem5  27476  pjsdi2i  27489  pjclem3  27529  pjci  27532  golem1  27603  iunrdx  27861  ofresid  27925  mpteq12df  27938  resmptf  27939  f1od2  27994  gsumvsca1  28225  gsumvsca2  28226  rhmopp  28262  resv1r  28280  crefeq  28301  xrge0mulc1cn  28376  qqhval2  28415  rrhre  28451  esumeq12dvaf  28478  esumeq2  28483  esumf1o  28497  esumfzf  28516  esumss  28519  esumpfinvalf  28523  ofceq  28544  itgeq12dv  28774  ccatmulgnn0dir  29002  bnj956  29162  bnj1385  29218  bnj96  29250  bnj548  29282  bnj553  29283  bnj554  29284  bnj602  29300  bnj18eq1  29312  bnj1234  29396  bnj1296  29404  bnj1318  29408  bnj1442  29432  bnj1450  29433  cvmliftlem5  29586  cvmliftlem10  29591  cvmlift2lem9  29608  cvmliftphtlem  29614  mthmpps  29794  mpteq12d  29985  rdgprc  30014  dfrdg2  30015  trpredeq1  30034  trpredeq2  30035  trpredeq3  30036  wsuceq123  30070  wlimeq12  30075  altopthsn  30299  altxpeq1  30311  altxpeq2  30312  ee7.2aOLD  30693  bj-rabbida2  31049  bj-sngleq  31090  bj-tageq  31099  bj-projeq  31115  bj-projval  31119  bj-1upleq  31122  bj-pr1eq  31125  bj-pr2eq  31139  finixpnum  31410  ptrest  31420  mbfposadd  31434  cnambfre  31435  iblabsnclem  31451  ftc1anclem1  31463  heiborlem4  31592  heiborlem6  31594  mpt2bi123f  31853  iineq12f  31855  mptbi12f  31857  riotaclbgBAD  31978  toycom  31991  ldualvbase  32144  ldualfvadd  32146  ldualsca  32150  ldualsbase  32151  ldualsaddN  32152  ldualfvs  32154  ldual0  32165  ldual1  32166  ldualneg  32167  cdleme19f  33327  cdleme20m  33342  cdleme21k  33357  cdleme27b  33387  cdleme31so  33398  cdleme31sn  33399  cdleme31se  33401  cdleme31se2  33402  cdleme31sc  33403  cdleme31sde  33404  cdleme31fv  33409  cdleme40v  33488  cdleme43dN  33511  cdlemeg46ngfr  33537  ltrnco4  33758  tgrpbase  33765  tgrpopr  33766  erngbase  33820  erngfplus  33821  erngfmul  33824  erngbase-rN  33828  erngfplus-rN  33829  erngfmul-rN  33832  dvasca  34025  dvavbase  34032  dvafvadd  34033  dvafvsca  34035  tendocnv  34041  dvhsca  34102  dvhfplusr  34104  dvhvbase  34107  dvhfvadd  34111  dvhfvsca  34120  lcdvadd  34617  lcdsbase  34620  lcdsadd  34621  lcdvs  34623  lcd0  34628  lcd1  34629  lcdneg  34630  imaiinfv  34987  mapfzcons1  35011  rexrabdioph  35089  dnnumch1  35352  dnwech  35356  aomclem6  35367  pwssplit4  35397  pwfi2f1o  35406  pwfi2f1oOLD  35407  mendplusgfval  35498  mendvscafval  35503  uzmptshftfval  36099  dropab1  36204  dropab2  36205  csbunigOLD  36646  csbfv12gALTOLD  36647  csbxpgOLD  36648  csbresgOLD  36650  csbrngOLD  36651  csbima12gALTOLD  36652  itgsinexplem1  37120  wallispi2lem2  37222  fourierdlem36  37293  etransclem4  37389  afveq12d  37586  aoveq123d  37631  aovfundmoveq  37634  aovnuoveq  37644  aovvoveq  37645  aovovn0oveq  37647  resisresindm  37938  fsumsplitsndif  37975  rngccofvalALTV  38306  ringccofvalALTV  38369  rhmsubclem2  38406  rhmsubcALTVlem2  38425  xpprsng  38432  aacllem  38860