Theorem 3eqtr4g 2795

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

Hypotheses

Ref	Expression
3eqtr4g.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr4g.2	⊢ 𝐶 = 𝐴
3eqtr4g.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3eqtr4g	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr4g

Step	Hyp	Ref	Expression
1		3eqtr4g.2	. . 3 ⊢ 𝐶 = 𝐴
2		3eqtr4g.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	eqtrid 2782	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2788	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2727

This theorem is referenced by:  rabbidva2  3400  rabbida4  3423  rabeqf  3432  csbeq1  3851  csbeq2  3853  csbeq2d  3854  csbeq2dv  3855  difeq1  4070  difeq2  4071  uneq2  4113  ineq1  4164  ineq2  4165  symdifeq1  4206  symdifeq2  4207  dfrab3ss  4274  csbprc  4360  csbnestgfw  4373  csbnestgf  4378  disjssun  4419  ifeq1  4482  ifeq2  4483  pweqALT  4568  sneq  4589  rabsneq  4598  csbsng  4664  csbprg  4665  preq1  4689  preq2  4690  tpeq1  4698  tpeq2  4699  tpeq3  4700  prprc1  4721  tpprceq3  4759  opeq1  4828  opeq2  4829  oteq1  4837  oteq2  4838  oteq3  4839  csbopg  4846  uniprg  4878  csbuni  4892  inteq  4904  iineq1  4963  iineq2  4966  iuneq12df  4972  iuneq12d  4975  dfiin2g  4985  iinrab  5023  iinin1  5033  iinxprg  5043  iununi  5053  opabbid  5162  opabbidv  5163  mpteq12da  5180  mpteq12f  5182  mpteq12dva  5183  csbmpt12  5504  xpeq1  5637  xpeq2  5644  rneq  5884  reseq1  5931  reseq2  5932  resima2  5974  resindm  5988  resmpt  5995  resmptf  5997  imaeq1  6013  imaeq2  6014  mptcnv  6095  xpdisj1  6118  xpdisj2  6119  resdisj  6126  dmpropg  6172  rnpropg  6179  cores  6206  cores2  6217  xpco  6246  predeq123  6259  csbpredg  6264  sspred  6267  predres  6296  suceqd  6383  sucprc  6394  iotaeq  6459  iotabi  6460  fntpg  6551  imain  6576  f1oprswap  6818  fveq1  6832  fveq2  6833  fvres  6852  csbfv12  6878  fnimapr  6916  fnimatpd  6917  fvco2  6930  xpprsng  7085  residpr  7088  fsnunfv  7133  fsnunres  7134  funiunfv  7194  f1ofvswap  7252  fliftf  7261  isoini2  7285  eqfunressuc  7307  riotaeqdv  7316  riotabidv  7317  riotauni  7321  riotabidva  7334  snriota  7348  oveq  7364  oveq1  7365  oveq2  7366  oprabbid  7423  oprabbidv  7424  mpoeq123  7430  mpoeq123dva  7432  mpoeq3dva  7435  resmpo  7478  ovres  7524  f1ocnvd  7609  ofeqd  7624  ofreq  7626  fpar  8058  frecseq123  8224  csbfrecsg  8226  wrecseq123  8255  csbwrecsg  8260  onovuni  8274  recseq  8305  tfr2a  8326  rdgeq1  8342  rdgeq2  8343  rdgsucmptf  8359  frsucmpt  8369  seqomeq12  8385  seqomsuc  8388  omopthi  8589  eceq1  8675  eceq2  8677  qseq1  8695  qseq2  8696  uniqs  8712  snecg  8716  ecinxp  8731  qsinxp  8732  erovlem  8752  ecopovtrn  8759  ixpeq1  8848  unfi  9097  supeq1  9350  supeq2  9353  supeq3  9354  supeq123d  9355  infeq1  9382  infeq2  9385  infeq3  9386  infeq123d  9387  infiso  9415  oieq1  9419  oieq2  9420  ordtypelem1  9425  inf3lemc  9537  wemapwe  9608  ttrcleq  9620  r1sucg  9683  r1limg  9685  rankprb  9765  karden  9809  djueq12  9818  cardiun  9896  acneq  9955  alephlim  9979  alephsuc  9980  alephfplem2  10017  infpssrlem2  10216  fin23lem34  10258  fin23lem35  10259  zorn2lem1  10408  zorn2lem7  10414  fpwwe2lem5  10548  fpwwe2lem12  10555  addpiord  10797  mulpiord  10798  addpqnq  10851  mulpqnq  10854  addassnq  10871  mulassnq  10872  distrnq  10874  lterpq  10883  ltexnq  10888  ltsrpr  10990  00sr  11012  recexsrlem  11016  mulgt0sr  11018  addcnsrec  11056  mulcnsrec  11057  negeq  11374  csbnegg  11379  negsubdi  11439  mulneg1  11575  negfi  12093  deceq1  12614  deceq2  12615  xnegeq  13124  fseq1p1m1  13516  om2uzrdg  13881  uzrdgsuci  13885  seqeq1  13929  seqeq2  13930  seqeq3  13931  seqfeq4  13976  seqof  13984  hashprg  14320  hashtpg  14410  csbwrdg  14469  s1eq  14526  cats1co  14781  s2eqd  14788  s3eqd  14789  s4eqd  14790  s5eqd  14791  s6eqd  14792  s7eqd  14793  s8eqd  14794  xpcogend  14899  shftval  14999  limsupgle  15402  lo1eq  15493  rlimeq  15494  sumeq1  15614  sumeq2w  15617  sumeq2ii  15618  sumeq2sdv  15628  zsum  15643  sumss2  15651  fsumsplitsnun  15680  isumclim3  15684  fsumcom2  15699  incexclem  15761  incexc2  15763  isumshft  15764  prodeq1f  15831  prodeq1  15832  prodeq2w  15835  prodeq2ii  15836  prodeq2sdv  15848  zprod  15862  fprodm1s  15895  fprodp1s  15896  fprodcom2  15909  fprodsplitf  15913  iprodclim3  15925  ef0lem  16003  ruclem7  16163  sadcp1  16384  smupp1  16409  smueqlem  16419  algrp1  16503  dfphi2  16703  prmdiveq  16715  pceulem  16775  vdwlem6  16916  cshwsiun  17029  sloteq  17112  setsid  17136  elbasfv  17144  elbasov  17145  imastset  17445  imasvscaval  17461  isoval  17691  funcoppc  17801  fulloppc  17850  fuccofval  17888  natpropd  17905  catccofval  18030  xpchomfval  18104  xpccofval  18107  lubfval  18273  glbfval  18286  chneq1  18537  chneq2  18538  grpidpropd  18589  gsumpropd2lem  18606  frmdplusg  18781  efmndplusg  18807  grpinvpropd  18947  grpsubpropd  18977  grpsubpropd2  18978  mulgpropd  19048  ecqusaddd  19123  oppgmnd  19285  sylow1lem2  19530  sylow3lem1  19558  prds1  20260  pwsmgp  20264  opprrng  20283  rngidpropd  20353  dvdsrpropd  20354  unitpropd  20355  invrpropd  20356  rhm1  20426  rhmopp  20444  rhmsubclem2  20621  lmhmpropd  21027  lidlrsppropd  21201  rngqiprnglinlem2  21249  lpival  21281  pzriprnglem11  21448  zrhpropd  21471  znle  21493  frlmplusgval  21721  frlmvscafval  21723  ressascl  21854  asclpropd  21855  aspval2  21856  psrbas  21891  psrplusg  21894  psrmulr  21900  psrvscafval  21906  resspsrbas  21931  ressmplbas2  21984  opsrle  22004  opsrbaslem  22006  vr1val  22134  ressply1add  22172  ressply1mul  22173  ressply1vsca  22174  psrplusgpropd  22178  mplbaspropd  22179  psropprmul  22180  ply1baspropd  22185  ply1plusgpropd  22186  ply1sca2  22196  ply1ascl0  22197  ply1ascl1  22198  subrgvr1  22205  coe1mul2lem2  22212  ply1coe1eq  22246  evls1addd  22317  evls1muld  22318  evls1vsca  22319  rhmply1vr1  22333  rhmply1vsca  22334  mamudi  22349  mamudir  22350  matrcl  22358  oftpos  22398  mattpos1  22402  mdetfval  22532  mdetrlin  22548  mdetrsca  22549  mdetrsca2  22550  mdetrlin2  22553  mdetunilem5  22562  madufval  22583  madugsum  22589  idmatidpmat  22683  cpmidpmat  22819  cncmp  23338  2ndcsep  23405  llyeq  23416  nllyeq  23417  xkouni  23545  hmphindis  23743  xkocnv  23760  ptcmplem2  23999  snclseqg  24062  prdstmdd  24070  ustexsym  24162  ucnextcn  24249  metreslem  24308  comet  24459  nrmmetd  24520  nmpropd  24540  isngp3  24544  ngpds  24550  subgnm  24579  tngnm  24597  idnghm  24689  cnmetdval  24716  cnmpopc  24880  htpyco2  24936  phtpyco2  24947  clsocv  25208  rrxprds  25347  rrxnm  25349  rrxplusgvscavalb  25353  ovolunlem1a  25455  voliunlem3  25511  ioombl1lem4  25520  uniioombllem4  25545  itg11  25650  itgeq1f  25730  itgeq1fOLD  25731  itgeq1  25732  itgeq2  25737  iblss2  25765  itgss  25771  itgeqa  25773  itgfsum  25786  itgsplit  25795  ditgeq1  25807  ditgeq2  25808  ditgeq3  25809  dvcmulf  25906  dvmptfsum  25937  dvcnvrelem2  25981  mdegfval  26025  mdegpropd  26047  deg1propd  26049  plyeq0  26174  coe11  26216  dgrlt  26230  dgradd2  26232  dgrmulc  26235  dvply1  26249  fta1lem  26273  pserulm  26389  rlimcnp2  26934  jensenlem1  26955  basellem5  27053  dchrbas  27204  dchrrcl  27209  dchrplusg  27216  dchrfi  27224  lgsdi  27303  lgseisenlem2  27345  lgsquadlem3  27351  dchrmusumlema  27462  rpvmasum2  27481  dchrisum0lema  27483  pntlemg  27567  nosupbnd2lem1  27685  lruneq  27887  addsval  27942  mulsval  28089  seqseq123d  28265  colperpexlem2  28784  axlowdimlem13  29008  uhgrvtxedgiedgb  29190  nb3grprlem1  29434  crctcshlem2  29872  wpthswwlks2on  30018  clwlknf1oclwwlkn  30140  frgrncvvdeq  30365  avril1  30519  0vfval  30662  imsval  30741  imsdval  30742  bcseqi  31176  normpythi  31198  cm0  31665  fh1  31674  pjcji  31740  opsqrlem5  32200  pjsdi2i  32213  pjclem3  32253  pjci  32256  golem1  32327  iuneq12daf  32611  iunrdx  32618  ofresid  32700  cnvprop  32754  coprprop  32757  f1od2  32777  dp2eq1  32933  dp2eq2  32934  fzto1st1  33163  gsumvsca1  33287  gsumvsca2  33288  urpropd  33292  resv1r  33399  nsgqusf1olem2  33474  oppr2idl  33546  opprqus0g  33550  ressply1evls1  33625  esplyfvn  33712  vietalem  33714  lindsunlem  33760  fedgmullem1  33765  fedgmullem2  33766  fedgmul  33767  fldsdrgfldext2  33798  fldextrspunlem1  33811  fldextrspunfld  33812  algextdeglem4  33856  crefeq  33981  rspectopn  34003  xrge0mulc1cn  34077  qqhval2  34118  esumeq12dvaf  34167  esumeq2  34172  esumf1o  34186  esumfzf  34205  esumss  34208  esumpfinvalf  34212  ofceq  34233  carsgclctunlem1  34453  itgeq12dv  34462  ccatmulgnn0dir  34678  breprexpnat  34770  bnj956  34911  bnj1385  34967  bnj96  35000  bnj548  35032  bnj553  35033  bnj554  35034  bnj602  35050  bnj18eq1  35062  bnj1234  35148  bnj1296  35156  bnj1318  35160  bnj1442  35184  bnj1450  35185  cvmliftlem5  35462  cvmliftlem10  35467  cvmlift2lem9  35484  cvmliftphtlem  35490  satfdm  35542  mthmpps  35755  rdgprc  35965  dfrdg2  35966  wsuceq123  35985  wlimeq12  35990  altopthsn  36134  altxpeq1  36146  altxpeq2  36147  ixpeq12dv  36389  prodeq12sdv  36391  itgeq12sdv  36392  ditgeq123dv  36394  cbvcsbdavw  36432  cbvcsbdavw2  36433  cbvrabdavw  36434  cbviundavw  36435  cbviindavw  36436  cbvopab1davw  36437  cbvopab2davw  36438  cbvopabdavw  36439  cbvmptdavw  36440  cbviotadavw  36442  cbvriotadavw  36443  cbvoprab1davw  36444  cbvoprab2davw  36445  cbvoprab3davw  36446  cbvoprab123davw  36447  cbvoprab12davw  36448  cbvoprab23davw  36449  cbvoprab13davw  36450  cbvixpdavw  36451  cbvsumdavw  36452  cbvproddavw  36453  cbvitgdavw  36454  cbvditgdavw  36455  cbvrabdavw2  36458  cbviundavw2  36459  cbviindavw2  36460  cbvmptdavw2  36461  cbvriotadavw2  36463  cbvmpodavw2  36464  cbvmpo1davw2  36465  cbvmpo2davw2  36466  cbvixpdavw2  36467  cbvsumdavw2  36468  cbvproddavw2  36469  cbvitgdavw2  36470  cbvditgdavw2  36471  ee7.2aOLD  36634  bj-sngleq  37141  bj-tageq  37150  bj-projeq  37166  bj-projval  37170  bj-1upleq  37173  bj-pr1eq  37176  bj-pr2eq  37190  bj-evaleq  37246  bj-imafv  37425  csbrecsg  37502  csbrdgg  37503  csboprabg  37504  csbmpo123  37505  finxpeq1  37560  finxpeq2  37561  csbfinxpg  37562  finxpreclem4  37568  cureq  37766  unceq  37767  uncov  37771  unccur  37773  finixpnum  37775  ptrest  37789  poimirlem3  37793  poimirlem9  37799  poimirlem15  37805  poimirlem16  37806  poimirlem26  37816  poimirlem27  37817  mbfposadd  37837  cnambfre  37838  iblabsnclem  37853  ftc1anclem1  37863  heiborlem4  37984  heiborlem6  37986  mpobi123f  38332  iineq12f  38334  mptbi12f  38336  eccnvepres  38456  xrneq1  38566  xrneq2  38569  shiftstableeq2  38653  cosseq  38686  redundss3  38882  riotaclbgBAD  39249  toycom  39268  ldualvbase  39421  ldualfvadd  39423  ldualsca  39427  ldualsbase  39428  ldualsaddN  39429  ldualfvs  39431  ldual0  39442  ldual1  39443  ldualneg  39444  cdleme19f  40603  cdleme20m  40618  cdleme21k  40633  cdleme27b  40663  cdleme31so  40674  cdleme31sn  40675  cdleme31se  40677  cdleme31se2  40678  cdleme31sc  40679  cdleme31sde  40680  cdleme31fv  40685  cdleme40v  40764  cdleme43dN  40787  cdlemeg46ngfr  40813  ltrnco4  41034  tgrpbase  41041  tgrpopr  41042  erngbase  41096  erngfplus  41097  erngfmul  41100  erngbase-rN  41104  erngfplus-rN  41105  erngfmul-rN  41108  dvasca  41301  dvavbase  41308  dvafvadd  41309  dvafvsca  41311  tendocnv  41316  dvhsca  41377  dvhfplusr  41379  dvhvbase  41382  dvhfvadd  41386  dvhfvsca  41395  lcdvadd  41892  lcdsbase  41895  lcdsadd  41896  lcdvs  41898  lcd0  41903  lcd1  41904  lcdneg  41905  fsuppind  42870  imaiinfv  42972  mapfzcons1  42996  rexrabdioph  43073  dnnumch1  43323  dnwech  43327  aomclem6  43338  pwssplit4  43368  pwfi2f1o  43375  mendplusgfval  43460  mendvscafval  43465  harval3  43816  dssmapntrcls  44406  scotteqd  44515  colleq12d  44531  uzmptshftfval  44624  dropab1  44724  dropab2  44725  iineq12dv  45387  rabbida2  45413  rabbida3  45416  itgsinexplem1  46235  wallispi2lem2  46353  fourierdlem36  46424  etransclem4  46519  fcoreslem1  47346  afveq12d  47416  aoveq123d  47461  aovfundmoveq  47464  aovnuoveq  47474  aovvoveq  47475  aovovn0oveq  47477  afv2eq12d  47498  fsumsplitsndif  47656  rngccofvalALTV  48553  rhmsubcALTVlem2  48565  ringccofvalALTV  48587  itscnhlinecirc02plem2  49066  oppfrcl3  49412  oppf1st2nd  49413  uppropd  49463  natoppf  49511  catcrcl  49677  lmdpropd  49939  cmdpropd  49940  lmddu  49949  cmddu  49950  setrecseq  49967  aacllem  50083