Theorem 3eqtr4g 2789

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 2776	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2782	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  rabbidva2  3404  rabbida4  3428  rabeqf  3437  csbeq1  3862  csbeq2  3864  csbeq2d  3865  csbeq2dv  3866  difeq1  4078  difeq2  4079  uneq2  4121  ineq1  4172  ineq2  4173  symdifeq1  4214  symdifeq2  4215  dfrab3ss  4282  csbprc  4368  csbnestgfw  4381  csbnestgf  4386  disjssun  4427  ifeq1  4488  ifeq2  4489  pweqALT  4574  sneq  4595  rabsneq  4604  csbsng  4668  csbprg  4669  preq1  4693  preq2  4694  tpeq1  4702  tpeq2  4703  tpeq3  4704  prprc1  4725  tpprceq3  4764  opeq1  4833  opeq2  4834  oteq1  4842  oteq2  4843  oteq3  4844  csbopg  4851  uniprg  4883  csbuni  4896  inteq  4909  iineq1  4969  iineq2  4972  iuneq12df  4978  iuneq12d  4981  dfiin2g  4991  iinrab  5028  iinin1  5038  iinxprg  5048  iununi  5058  opabbid  5167  opabbidv  5168  mpteq12da  5185  mpteq12f  5187  mpteq12dva  5188  csbmpt12  5512  xpeq1  5645  xpeq2  5652  rneq  5889  reseq1  5933  reseq2  5934  resima2  5976  resindm  5990  resmpt  5997  resmptf  5999  imaeq1  6015  imaeq2  6016  mptcnv  6100  xpdisj1  6122  xpdisj2  6123  resdisj  6130  dmpropg  6176  rnpropg  6183  cores  6210  cores2  6220  xpco  6250  predeq123  6263  csbpredg  6268  sspred  6271  predres  6300  suceqd  6387  sucprc  6398  iotaeq  6464  iotabi  6465  fntpg  6560  imain  6585  f1oprswap  6826  fveq1  6839  fveq2  6840  fvres  6859  csbfv12  6888  fnimapr  6926  fnimatpd  6927  fvco2  6940  xpprsng  7094  residpr  7097  fsnunfv  7143  fsnunres  7144  funiunfv  7204  f1ofvswap  7263  fliftf  7272  isoini2  7296  eqfunressuc  7318  riotaeqdv  7327  riotabidv  7328  riotauni  7332  riotabidva  7345  snriota  7359  oveq  7375  oveq1  7376  oveq2  7377  oprabbid  7434  oprabbidv  7435  mpoeq123  7441  mpoeq123dva  7443  mpoeq3dva  7446  resmpo  7489  ovres  7535  f1ocnvd  7620  ofeqd  7635  ofreq  7637  fpar  8072  frecseq123  8238  csbfrecsg  8240  wrecseq123  8269  csbwrecsg  8274  onovuni  8288  recseq  8319  tfr2a  8340  rdgeq1  8356  rdgeq2  8357  rdgsucmptf  8373  frsucmpt  8383  seqomeq12  8399  seqomsuc  8402  omopthi  8602  eceq1  8687  eceq2  8689  qseq1  8707  qseq2  8708  uniqs  8724  ecinxp  8742  qsinxp  8743  erovlem  8763  ecopovtrn  8770  ixpeq1  8858  unfi  9112  supeq1  9372  supeq2  9375  supeq3  9376  supeq123d  9377  infeq1  9404  infeq2  9407  infeq3  9408  infeq123d  9409  infiso  9437  oieq1  9441  oieq2  9442  ordtypelem1  9447  inf3lemc  9557  wemapwe  9628  ttrcleq  9640  r1sucg  9700  r1limg  9702  rankprb  9782  karden  9826  djueq12  9835  cardiun  9913  acneq  9974  alephlim  9998  alephsuc  9999  alephfplem2  10036  infpssrlem2  10235  fin23lem34  10277  fin23lem35  10278  zorn2lem1  10427  zorn2lem7  10433  fpwwe2lem5  10566  fpwwe2lem12  10573  addpiord  10815  mulpiord  10816  addpqnq  10869  mulpqnq  10872  addassnq  10889  mulassnq  10890  distrnq  10892  lterpq  10901  ltexnq  10906  ltsrpr  11008  00sr  11030  recexsrlem  11034  mulgt0sr  11036  addcnsrec  11074  mulcnsrec  11075  negeq  11391  csbnegg  11396  negsubdi  11456  mulneg1  11592  negfi  12110  deceq1  12632  deceq2  12633  xnegeq  13145  fseq1p1m1  13537  om2uzrdg  13899  uzrdgsuci  13903  seqeq1  13947  seqeq2  13948  seqeq3  13949  seqfeq4  13994  seqof  14002  hashprg  14338  hashtpg  14428  csbwrdg  14487  s1eq  14543  cats1co  14799  s2eqd  14806  s3eqd  14807  s4eqd  14808  s5eqd  14809  s6eqd  14810  s7eqd  14811  s8eqd  14812  xpcogend  14917  shftval  15017  limsupgle  15420  lo1eq  15511  rlimeq  15512  sumeq1  15632  sumeq2w  15635  sumeq2ii  15636  sumeq2sdv  15646  zsum  15661  sumss2  15669  fsumsplitsnun  15698  isumclim3  15702  fsumcom2  15717  incexclem  15779  incexc2  15781  isumshft  15782  prodeq1f  15849  prodeq1  15850  prodeq2w  15853  prodeq2ii  15854  prodeq2sdv  15866  zprod  15880  fprodm1s  15913  fprodp1s  15914  fprodcom2  15927  fprodsplitf  15931  iprodclim3  15943  ef0lem  16021  ruclem7  16181  sadcp1  16402  smupp1  16427  smueqlem  16437  algrp1  16521  dfphi2  16721  prmdiveq  16733  pceulem  16793  vdwlem6  16934  cshwsiun  17047  sloteq  17130  setsid  17154  elbasfv  17162  elbasov  17163  imastset  17462  imasvscaval  17478  isoval  17708  funcoppc  17818  fulloppc  17867  fuccofval  17905  natpropd  17922  catccofval  18047  xpchomfval  18121  xpccofval  18124  lubfval  18290  glbfval  18303  grpidpropd  18572  gsumpropd2lem  18589  frmdplusg  18764  efmndplusg  18790  grpinvpropd  18930  grpsubpropd  18960  grpsubpropd2  18961  mulgpropd  19031  ecqusaddd  19107  oppgmnd  19269  sylow1lem2  19514  sylow3lem1  19542  prds1  20244  pwsmgp  20248  opprrng  20266  rngidpropd  20336  dvdsrpropd  20337  unitpropd  20338  invrpropd  20339  rhm1  20410  rhmopp  20430  rhmsubclem2  20607  lmhmpropd  21013  lidlrsppropd  21187  rngqiprnglinlem2  21235  lpival  21267  pzriprnglem11  21434  zrhpropd  21457  znle  21479  frlmplusgval  21707  frlmvscafval  21709  ressascl  21839  asclpropd  21840  aspval2  21841  psrbas  21876  psrplusg  21879  psrmulr  21885  psrvscafval  21891  resspsrbas  21917  ressmplbas2  21968  opsrle  21988  opsrbaslem  21990  vr1val  22110  ressply1add  22148  ressply1mul  22149  ressply1vsca  22150  psrplusgpropd  22154  mplbaspropd  22155  psropprmul  22156  ply1baspropd  22161  ply1plusgpropd  22162  ply1sca2  22172  ply1ascl0  22173  ply1ascl1  22174  subrgvr1  22181  coe1mul2lem2  22188  ply1coe1eq  22221  evls1addd  22292  evls1muld  22293  evls1vsca  22294  rhmply1vr1  22308  rhmply1vsca  22309  mamudi  22324  mamudir  22325  matrcl  22333  oftpos  22373  mattpos1  22377  mdetfval  22507  mdetrlin  22523  mdetrsca  22524  mdetrsca2  22525  mdetrlin2  22528  mdetunilem5  22537  madufval  22558  madugsum  22564  idmatidpmat  22658  cpmidpmat  22794  cncmp  23313  2ndcsep  23380  llyeq  23391  nllyeq  23392  xkouni  23520  hmphindis  23718  xkocnv  23735  ptcmplem2  23974  snclseqg  24037  prdstmdd  24045  ustexsym  24137  ucnextcn  24225  metreslem  24284  comet  24435  nrmmetd  24496  nmpropd  24516  isngp3  24520  ngpds  24526  subgnm  24555  tngnm  24573  idnghm  24665  cnmetdval  24692  cnmpopc  24856  htpyco2  24912  phtpyco2  24923  clsocv  25184  rrxprds  25323  rrxnm  25325  rrxplusgvscavalb  25329  ovolunlem1a  25431  voliunlem3  25487  ioombl1lem4  25496  uniioombllem4  25521  itg11  25626  itgeq1f  25706  itgeq1fOLD  25707  itgeq1  25708  itgeq2  25713  iblss2  25741  itgss  25747  itgeqa  25749  itgfsum  25762  itgsplit  25771  ditgeq1  25783  ditgeq2  25784  ditgeq3  25785  dvcmulf  25882  dvmptfsum  25913  dvcnvrelem2  25957  mdegfval  26001  mdegpropd  26023  deg1propd  26025  plyeq0  26150  coe11  26192  dgrlt  26206  dgradd2  26208  dgrmulc  26211  dvply1  26225  fta1lem  26249  pserulm  26365  rlimcnp2  26910  jensenlem1  26931  basellem5  27029  dchrbas  27180  dchrrcl  27185  dchrplusg  27192  dchrfi  27200  lgsdi  27279  lgseisenlem2  27321  lgsquadlem3  27327  dchrmusumlema  27438  rpvmasum2  27457  dchrisum0lema  27459  pntlemg  27543  nosupbnd2lem1  27661  lruneq  27857  addsval  27910  mulsval  28053  seqseq123d  28221  colperpexlem2  28712  axlowdimlem13  28935  uhgrvtxedgiedgb  29117  nb3grprlem1  29361  crctcshlem2  29799  wpthswwlks2on  29942  clwlknf1oclwwlkn  30064  frgrncvvdeq  30289  avril1  30443  0vfval  30586  imsval  30665  imsdval  30666  bcseqi  31100  normpythi  31122  cm0  31589  fh1  31598  pjcji  31664  opsqrlem5  32124  pjsdi2i  32137  pjclem3  32177  pjci  32180  golem1  32251  iuneq12daf  32536  iunrdx  32543  ofresid  32617  cnvprop  32670  coprprop  32673  f1od2  32695  dp2eq1  32844  dp2eq2  32845  fzto1st1  33075  gsumvsca1  33196  gsumvsca2  33197  urpropd  33200  resv1r  33305  nsgqusf1olem2  33379  oppr2idl  33451  opprqus0g  33455  ressply1evls1  33528  lindsunlem  33614  fedgmullem1  33619  fedgmullem2  33620  fedgmul  33621  fldsdrgfldext2  33652  fldextrspunlem1  33664  fldextrspunfld  33665  algextdeglem4  33704  crefeq  33829  rspectopn  33851  xrge0mulc1cn  33925  qqhval2  33966  esumeq12dvaf  34015  esumeq2  34020  esumf1o  34034  esumfzf  34053  esumss  34056  esumpfinvalf  34060  ofceq  34081  carsgclctunlem1  34302  itgeq12dv  34311  ccatmulgnn0dir  34527  breprexpnat  34619  bnj956  34760  bnj1385  34816  bnj96  34849  bnj548  34881  bnj553  34882  bnj554  34883  bnj602  34899  bnj18eq1  34911  bnj1234  34997  bnj1296  35005  bnj1318  35009  bnj1442  35033  bnj1450  35034  cvmliftlem5  35270  cvmliftlem10  35275  cvmlift2lem9  35292  cvmliftphtlem  35298  satfdm  35350  mthmpps  35563  rdgprc  35776  dfrdg2  35777  wsuceq123  35796  wlimeq12  35801  altopthsn  35943  altxpeq1  35955  altxpeq2  35956  ixpeq12dv  36198  prodeq12sdv  36200  itgeq12sdv  36201  ditgeq123dv  36203  cbvcsbdavw  36241  cbvcsbdavw2  36242  cbvrabdavw  36243  cbviundavw  36244  cbviindavw  36245  cbvopab1davw  36246  cbvopab2davw  36247  cbvopabdavw  36248  cbvmptdavw  36249  cbviotadavw  36251  cbvriotadavw  36252  cbvoprab1davw  36253  cbvoprab2davw  36254  cbvoprab3davw  36255  cbvoprab123davw  36256  cbvoprab12davw  36257  cbvoprab23davw  36258  cbvoprab13davw  36259  cbvixpdavw  36260  cbvsumdavw  36261  cbvproddavw  36262  cbvitgdavw  36263  cbvditgdavw  36264  cbvrabdavw2  36267  cbviundavw2  36268  cbviindavw2  36269  cbvmptdavw2  36270  cbvriotadavw2  36272  cbvmpodavw2  36273  cbvmpo1davw2  36274  cbvmpo2davw2  36275  cbvixpdavw2  36276  cbvsumdavw2  36277  cbvproddavw2  36278  cbvitgdavw2  36279  cbvditgdavw2  36280  ee7.2aOLD  36443  bj-sngleq  36949  bj-tageq  36958  bj-projeq  36974  bj-projval  36978  bj-1upleq  36981  bj-pr1eq  36984  bj-pr2eq  36998  bj-evaleq  37054  bj-imafv  37233  csbrecsg  37310  csbrdgg  37311  csboprabg  37312  csbmpo123  37313  finxpeq1  37368  finxpeq2  37369  csbfinxpg  37370  finxpreclem4  37376  cureq  37584  unceq  37585  uncov  37589  unccur  37591  finixpnum  37593  ptrest  37607  poimirlem3  37611  poimirlem9  37617  poimirlem15  37623  poimirlem16  37624  poimirlem26  37634  poimirlem27  37635  mbfposadd  37655  cnambfre  37656  iblabsnclem  37671  ftc1anclem1  37681  heiborlem4  37802  heiborlem6  37804  mpobi123f  38150  iineq12f  38152  mptbi12f  38154  eccnvepres  38262  xrneq1  38357  xrneq2  38360  cosseq  38411  redundss3  38613  riotaclbgBAD  38941  toycom  38960  ldualvbase  39113  ldualfvadd  39115  ldualsca  39119  ldualsbase  39120  ldualsaddN  39121  ldualfvs  39123  ldual0  39134  ldual1  39135  ldualneg  39136  cdleme19f  40296  cdleme20m  40311  cdleme21k  40326  cdleme27b  40356  cdleme31so  40367  cdleme31sn  40368  cdleme31se  40370  cdleme31se2  40371  cdleme31sc  40372  cdleme31sde  40373  cdleme31fv  40378  cdleme40v  40457  cdleme43dN  40480  cdlemeg46ngfr  40506  ltrnco4  40727  tgrpbase  40734  tgrpopr  40735  erngbase  40789  erngfplus  40790  erngfmul  40793  erngbase-rN  40797  erngfplus-rN  40798  erngfmul-rN  40801  dvasca  40994  dvavbase  41001  dvafvadd  41002  dvafvsca  41004  tendocnv  41009  dvhsca  41070  dvhfplusr  41072  dvhvbase  41075  dvhfvadd  41079  dvhfvsca  41088  lcdvadd  41585  lcdsbase  41588  lcdsadd  41589  lcdvs  41591  lcd0  41596  lcd1  41597  lcdneg  41598  fsuppind  42572  imaiinfv  42675  mapfzcons1  42699  rexrabdioph  42776  dnnumch1  43027  dnwech  43031  aomclem6  43042  pwssplit4  43072  pwfi2f1o  43079  mendplusgfval  43164  mendvscafval  43169  harval3  43521  dssmapntrcls  44111  scotteqd  44220  colleq12d  44236  uzmptshftfval  44329  dropab1  44430  dropab2  44431  iineq12dv  45094  rabbida2  45120  rabbida3  45123  itgsinexplem1  45946  wallispi2lem2  46064  fourierdlem36  46135  etransclem4  46230  fcoreslem1  47058  afveq12d  47128  aoveq123d  47173  aovfundmoveq  47176  aovnuoveq  47186  aovvoveq  47187  aovovn0oveq  47189  afv2eq12d  47210  fsumsplitsndif  47368  rngccofvalALTV  48252  rhmsubcALTVlem2  48264  ringccofvalALTV  48286  itscnhlinecirc02plem2  48766  oppfrcl3  49113  oppf1st2nd  49114  uppropd  49164  natoppf  49212  catcrcl  49378  lmdpropd  49640  cmdpropd  49641  lmddu  49650  cmddu  49651  setrecseq  49668  aacllem  49784