Theorem 3eqtr4g 2802

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 2789	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2795	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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  rabbidva2  3438  rabbida4  3462  rabeqf  3472  csbeq1  3902  csbeq2  3904  csbeq2d  3905  csbeq2dv  3906  difeq1  4119  difeq2  4120  uneq2  4162  ineq1  4213  ineq2  4214  symdifeq1  4255  symdifeq2  4256  dfrab3ss  4323  csbprc  4409  csbnestgfw  4422  csbnestgf  4427  disjssun  4468  ifeq1  4529  ifeq2  4530  pweqALT  4615  sneq  4636  rabsneq  4644  csbsng  4708  csbprg  4709  preq1  4733  preq2  4734  tpeq1  4742  tpeq2  4743  tpeq3  4744  prprc1  4765  tpprceq3  4804  opeq1  4873  opeq2  4874  oteq1  4882  oteq2  4883  oteq3  4884  csbopg  4891  uniprg  4923  csbuni  4936  inteq  4949  iineq1  5009  iineq2  5012  iuneq12df  5018  iuneq12d  5021  dfiin2g  5032  iinrab  5069  iinin1  5079  iinxprg  5089  iununi  5099  opabbid  5208  opabbidv  5209  mpteq12da  5227  mpteq12dfOLD  5229  mpteq12f  5230  mpteq12dva  5231  csbmpt12  5562  xpeq1  5699  xpeq2  5706  rneq  5947  reseq1  5991  reseq2  5992  resima2  6034  resindm  6048  resmpt  6055  resmptf  6057  imaeq1  6073  imaeq2  6074  mptcnv  6159  xpdisj1  6181  xpdisj2  6182  resdisj  6189  dmpropg  6235  rnpropg  6242  cores  6269  cores2  6279  xpco  6309  predeq123  6322  csbpredg  6327  sspred  6330  predres  6360  suceq  6450  sucprc  6460  iotaeq  6526  iotabi  6527  fntpg  6626  imain  6651  f1oprswap  6892  fveq1  6905  fveq2  6906  fvres  6925  csbfv12  6954  fnimapr  6992  fnimatpd  6993  fvco2  7006  xpprsng  7160  residpr  7163  fsnunfv  7207  fsnunres  7208  funiunfv  7268  f1ofvswap  7326  fliftf  7335  isoini2  7359  eqfunressuc  7381  riotaeqdv  7389  riotabidv  7390  riotauni  7394  riotabidva  7407  snriota  7421  oveq  7437  oveq1  7438  oveq2  7439  oprabbid  7498  oprabbidv  7499  mpoeq123  7505  mpoeq123dva  7507  mpoeq3dva  7510  resmpo  7553  ovres  7599  f1ocnvd  7684  ofeqd  7699  ofreq  7701  fpar  8141  frecseq123  8307  csbfrecsg  8309  wrecseq123  8339  wrecseq123OLD  8340  csbwrecsg  8346  onovuni  8382  recseq  8414  tfr2a  8435  rdgeq1  8451  rdgeq2  8452  rdgsucmptf  8468  frsucmpt  8478  seqomeq12  8494  seqomsuc  8497  omopthi  8699  eceq1  8784  eceq2  8786  qseq1  8801  qseq2  8802  uniqs  8817  ecinxp  8832  qsinxp  8833  erovlem  8853  ecopovtrn  8860  ixpeq1  8948  unfi  9211  supeq1  9485  supeq2  9488  supeq3  9489  supeq123d  9490  infeq1  9516  infeq2  9519  infeq3  9520  infeq123d  9521  infiso  9548  oieq1  9552  oieq2  9553  ordtypelem1  9558  inf3lemc  9666  wemapwe  9737  ttrcleq  9749  r1sucg  9809  r1limg  9811  rankprb  9891  karden  9935  djueq12  9944  cardiun  10022  acneq  10083  alephlim  10107  alephsuc  10108  alephfplem2  10145  infpssrlem2  10344  fin23lem34  10386  fin23lem35  10387  zorn2lem1  10536  zorn2lem7  10542  fpwwe2lem5  10675  fpwwe2lem12  10682  addpiord  10924  mulpiord  10925  addpqnq  10978  mulpqnq  10981  addassnq  10998  mulassnq  10999  distrnq  11001  lterpq  11010  ltexnq  11015  ltsrpr  11117  00sr  11139  recexsrlem  11143  mulgt0sr  11145  addcnsrec  11183  mulcnsrec  11184  negeq  11500  csbnegg  11505  negsubdi  11565  mulneg1  11699  negfi  12217  deceq1  12738  deceq2  12739  xnegeq  13249  fseq1p1m1  13638  om2uzrdg  13997  uzrdgsuci  14001  seqeq1  14045  seqeq2  14046  seqeq3  14047  seqfeq4  14092  seqof  14100  hashprg  14434  hashtpg  14524  csbwrdg  14582  s1eq  14638  cats1co  14895  s2eqd  14902  s3eqd  14903  s4eqd  14904  s5eqd  14905  s6eqd  14906  s7eqd  14907  s8eqd  14908  xpcogend  15013  shftval  15113  limsupgle  15513  lo1eq  15604  rlimeq  15605  sumeq1  15725  sumeq2w  15728  sumeq2ii  15729  sumeq2sdv  15739  zsum  15754  sumss2  15762  fsumsplitsnun  15791  isumclim3  15795  fsumcom2  15810  incexclem  15872  incexc2  15874  isumshft  15875  prodeq1f  15942  prodeq1  15943  prodeq2w  15946  prodeq2ii  15947  prodeq2sdv  15959  zprod  15973  fprodm1s  16006  fprodp1s  16007  fprodcom2  16020  fprodsplitf  16024  iprodclim3  16036  ef0lem  16114  ruclem7  16272  sadcp1  16492  smupp1  16517  smueqlem  16527  algrp1  16611  dfphi2  16811  prmdiveq  16823  pceulem  16883  vdwlem6  17024  cshwsiun  17137  sloteq  17220  setsid  17244  elbasfv  17253  elbasov  17254  imastset  17567  imasvscaval  17583  isoval  17809  funcoppc  17920  fulloppc  17969  fuccofval  18007  natpropd  18024  catccofval  18149  xpchomfval  18224  xpccofval  18227  lubfval  18395  glbfval  18408  grpidpropd  18675  gsumpropd2lem  18692  frmdplusg  18867  efmndplusg  18893  grpinvpropd  19033  grpsubpropd  19063  grpsubpropd2  19064  mulgpropd  19134  ecqusaddd  19210  oppgmnd  19373  sylow1lem2  19617  sylow3lem1  19645  prds1  20320  pwsmgp  20324  opprrng  20345  rngidpropd  20415  dvdsrpropd  20416  unitpropd  20417  invrpropd  20418  rhm1  20489  rhmopp  20509  rhmsubclem2  20686  lmhmpropd  21072  lidlrsppropd  21254  rngqiprnglinlem2  21302  lpival  21334  pzriprnglem11  21502  zrhpropd  21525  znle  21551  frlmplusgval  21784  frlmvscafval  21786  ressascl  21916  asclpropd  21917  aspval2  21918  psrbas  21953  psrplusg  21956  psrmulr  21962  psrvscafval  21968  resspsrbas  21994  ressmplbas2  22045  opsrle  22065  opsrbaslem  22067  opsrbaslemOLD  22068  vr1val  22193  ressply1add  22231  ressply1mul  22232  ressply1vsca  22233  psrplusgpropd  22237  mplbaspropd  22238  psropprmul  22239  ply1baspropd  22244  ply1plusgpropd  22245  ply1sca2  22255  ply1ascl0  22256  ply1ascl1  22257  subrgvr1  22264  coe1mul2lem2  22271  ply1coe1eq  22304  evls1addd  22375  evls1muld  22376  evls1vsca  22377  rhmply1vr1  22391  rhmply1vsca  22392  mamudi  22407  mamudir  22408  matrcl  22416  oftpos  22458  mattpos1  22462  mdetfval  22592  mdetrlin  22608  mdetrsca  22609  mdetrsca2  22610  mdetrlin2  22613  mdetunilem5  22622  madufval  22643  madugsum  22649  idmatidpmat  22743  cpmidpmat  22879  cncmp  23400  2ndcsep  23467  llyeq  23478  nllyeq  23479  xkouni  23607  hmphindis  23805  xkocnv  23822  ptcmplem2  24061  snclseqg  24124  prdstmdd  24132  ustexsym  24224  ucnextcn  24313  metreslem  24372  comet  24526  nrmmetd  24587  nmpropd  24607  isngp3  24611  ngpds  24617  subgnm  24646  tngnm  24672  idnghm  24764  cnmetdval  24791  cnmpopc  24955  htpyco2  25011  phtpyco2  25022  clsocv  25284  rrxprds  25423  rrxnm  25425  rrxplusgvscavalb  25429  ovolunlem1a  25531  voliunlem3  25587  ioombl1lem4  25596  uniioombllem4  25621  itg11  25726  itgeq1f  25806  itgeq1fOLD  25807  itgeq1  25808  itgeq2  25813  iblss2  25841  itgss  25847  itgeqa  25849  itgfsum  25862  itgsplit  25871  ditgeq1  25883  ditgeq2  25884  ditgeq3  25885  dvcmulf  25982  dvmptfsum  26013  dvcnvrelem2  26057  mdegfval  26101  mdegpropd  26123  deg1propd  26125  plyeq0  26250  coe11  26292  dgrlt  26306  dgradd2  26308  dgrmulc  26311  dvply1  26325  fta1lem  26349  pserulm  26465  rlimcnp2  27009  jensenlem1  27030  basellem5  27128  dchrbas  27279  dchrrcl  27284  dchrplusg  27291  dchrfi  27299  lgsdi  27378  lgseisenlem2  27420  lgsquadlem3  27426  dchrmusumlema  27537  rpvmasum2  27556  dchrisum0lema  27558  pntlemg  27642  nosupbnd2lem1  27760  lruneq  27944  addsval  27995  mulsval  28135  seqseq123d  28292  colperpexlem2  28739  axlowdimlem13  28969  uhgrvtxedgiedgb  29153  nb3grprlem1  29397  crctcshlem2  29838  wpthswwlks2on  29981  clwlknf1oclwwlkn  30103  frgrncvvdeq  30328  avril1  30482  0vfval  30625  imsval  30704  imsdval  30705  bcseqi  31139  normpythi  31161  cm0  31628  fh1  31637  pjcji  31703  opsqrlem5  32163  pjsdi2i  32176  pjclem3  32216  pjci  32219  golem1  32290  iuneq12daf  32569  iunrdx  32576  ofresid  32652  cnvprop  32705  coprprop  32708  f1od2  32732  dp2eq1  32855  dp2eq2  32856  fzto1st1  33122  gsumvsca1  33232  gsumvsca2  33233  urpropd  33236  resv1r  33368  nsgqusf1olem2  33442  oppr2idl  33514  opprqus0g  33518  lindsunlem  33675  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  fldsdrgfldext2  33713  fldextrspunlem1  33725  fldextrspunfld  33726  algextdeglem4  33761  crefeq  33844  rspectopn  33866  xrge0mulc1cn  33940  qqhval2  33983  esumeq12dvaf  34032  esumeq2  34037  esumf1o  34051  esumfzf  34070  esumss  34073  esumpfinvalf  34077  ofceq  34098  carsgclctunlem1  34319  itgeq12dv  34328  ccatmulgnn0dir  34557  breprexpnat  34649  bnj956  34790  bnj1385  34846  bnj96  34879  bnj548  34911  bnj553  34912  bnj554  34913  bnj602  34929  bnj18eq1  34941  bnj1234  35027  bnj1296  35035  bnj1318  35039  bnj1442  35063  bnj1450  35064  cvmliftlem5  35294  cvmliftlem10  35299  cvmlift2lem9  35316  cvmliftphtlem  35322  satfdm  35374  mthmpps  35587  rdgprc  35795  dfrdg2  35796  wsuceq123  35815  wlimeq12  35820  altopthsn  35962  altxpeq1  35974  altxpeq2  35975  ixpeq12dv  36217  prodeq12sdv  36219  itgeq12sdv  36220  ditgeq123dv  36222  cbvcsbdavw  36260  cbvcsbdavw2  36261  cbvrabdavw  36262  cbviundavw  36263  cbviindavw  36264  cbvopab1davw  36265  cbvopab2davw  36266  cbvopabdavw  36267  cbvmptdavw  36268  cbviotadavw  36270  cbvriotadavw  36271  cbvoprab1davw  36272  cbvoprab2davw  36273  cbvoprab3davw  36274  cbvoprab123davw  36275  cbvoprab12davw  36276  cbvoprab23davw  36277  cbvoprab13davw  36278  cbvixpdavw  36279  cbvsumdavw  36280  cbvproddavw  36281  cbvitgdavw  36282  cbvditgdavw  36283  cbvrabdavw2  36286  cbviundavw2  36287  cbviindavw2  36288  cbvmptdavw2  36289  cbvriotadavw2  36291  cbvmpodavw2  36292  cbvmpo1davw2  36293  cbvmpo2davw2  36294  cbvixpdavw2  36295  cbvsumdavw2  36296  cbvproddavw2  36297  cbvitgdavw2  36298  cbvditgdavw2  36299  ee7.2aOLD  36462  bj-sngleq  36968  bj-tageq  36977  bj-projeq  36993  bj-projval  36997  bj-1upleq  37000  bj-pr1eq  37003  bj-pr2eq  37017  bj-evaleq  37073  bj-imafv  37252  csbrecsg  37329  csbrdgg  37330  csboprabg  37331  csbmpo123  37332  finxpeq1  37387  finxpeq2  37388  csbfinxpg  37389  finxpreclem4  37395  cureq  37603  unceq  37604  uncov  37608  unccur  37610  finixpnum  37612  ptrest  37626  poimirlem3  37630  poimirlem9  37636  poimirlem15  37642  poimirlem16  37643  poimirlem26  37653  poimirlem27  37654  mbfposadd  37674  cnambfre  37675  iblabsnclem  37690  ftc1anclem1  37700  heiborlem4  37821  heiborlem6  37823  mpobi123f  38169  iineq12f  38171  mptbi12f  38173  eccnvepres  38281  uniqsALTV  38330  xrneq1  38378  xrneq2  38381  cosseq  38427  redundss3  38629  riotaclbgBAD  38955  toycom  38974  ldualvbase  39127  ldualfvadd  39129  ldualsca  39133  ldualsbase  39134  ldualsaddN  39135  ldualfvs  39137  ldual0  39148  ldual1  39149  ldualneg  39150  cdleme19f  40310  cdleme20m  40325  cdleme21k  40340  cdleme27b  40370  cdleme31so  40381  cdleme31sn  40382  cdleme31se  40384  cdleme31se2  40385  cdleme31sc  40386  cdleme31sde  40387  cdleme31fv  40392  cdleme40v  40471  cdleme43dN  40494  cdlemeg46ngfr  40520  ltrnco4  40741  tgrpbase  40748  tgrpopr  40749  erngbase  40803  erngfplus  40804  erngfmul  40807  erngbase-rN  40811  erngfplus-rN  40812  erngfmul-rN  40815  dvasca  41008  dvavbase  41015  dvafvadd  41016  dvafvsca  41018  tendocnv  41023  dvhsca  41084  dvhfplusr  41086  dvhvbase  41089  dvhfvadd  41093  dvhfvsca  41102  lcdvadd  41599  lcdsbase  41602  lcdsadd  41603  lcdvs  41605  lcd0  41610  lcd1  41611  lcdneg  41612  fsuppind  42600  imaiinfv  42704  mapfzcons1  42728  rexrabdioph  42805  dnnumch1  43056  dnwech  43060  aomclem6  43071  pwssplit4  43101  pwfi2f1o  43108  mendplusgfval  43193  mendvscafval  43198  harval3  43551  dssmapntrcls  44141  scotteqd  44256  colleq12d  44272  uzmptshftfval  44365  dropab1  44466  dropab2  44467  iineq12dv  45111  rabbida2  45137  rabbida3  45140  itgsinexplem1  45969  wallispi2lem2  46087  fourierdlem36  46158  etransclem4  46253  fcoreslem1  47075  afveq12d  47145  aoveq123d  47190  aovfundmoveq  47193  aovnuoveq  47203  aovvoveq  47204  aovovn0oveq  47206  afv2eq12d  47227  fsumsplitsndif  47360  rngccofvalALTV  48186  rhmsubcALTVlem2  48198  ringccofvalALTV  48220  itscnhlinecirc02plem2  48704  setrecseq  49204  aacllem  49320