Theorem 3eqtr4g 2801

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

Syntax hints:   → wi 4   = wceq 1548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733

This theorem is referenced by:  rabbidva2  3395  rabbida4  3418  csbeq1  3836  csbeq2  3838  csbeq2d  3839  csbeq2dv  3840  difeq1  4053  difeq2  4054  uneq2  4095  ineq1  4145  ineq2  4146  symdifeq1  4186  symdifeq2  4187  dfrab3ss  4254  csbprc  4340  csbnestgfw  4353  csbnestgf  4358  disjssun  4399  ifeq1  4461  ifeq2  4462  pweqALT  4547  sneq  4568  csbsng  4643  csbprg  4644  preq1  4668  preq2  4669  tpeq1  4677  tpeq2  4678  tpeq3  4679  prprc1  4700  tpprceq3  4740  opeq1  4807  opeq2  4808  oteq1  4816  oteq2  4817  oteq3  4818  csbopg  4825  uniprg  4857  csbuni  4871  inteq  4883  iineq1  4942  iineq2  4945  iuneq12df  4951  iuneq12d  4954  dfiin2g  4963  iinrab  5001  iinin1  5011  iinxprg  5021  iununi  5031  opabbid  5140  opabbidv  5141  mpteq12da  5158  mpteq12f  5160  mpteq12dva  5161  csbmpt12  5502  xpeq1  5635  xpeq2  5642  rneq  5885  reseq1  5932  reseq2  5933  resima2  5975  resindm  5989  resmpt  5996  resmptf  5998  imaeq1  6014  imaeq2  6015  mptcnv  6096  xpdisj1  6116  xpdisj2  6117  resdisj  6124  dmpropg  6170  rnpropg  6177  cores  6204  cores2  6215  xpco  6244  predeq123  6257  csbpredg  6262  sspred  6265  predres  6294  suceqd  6381  sucprc  6392  iotaeq  6457  iotabi  6458  fntpg  6549  imain  6574  f1oprswap  6816  fveq1  6830  fveq2  6831  fvres  6850  csbfv12  6876  fnimapr  6914  fnimatpd  6915  fvco2  6928  xpprsng  7086  residpr  7089  fsnunfv  7135  fsnunres  7136  funiunfv  7196  f1ofvswap  7254  fliftf  7263  isoini2  7287  eqfunressuc  7309  riotaeqdv  7318  riotabidv  7319  riotauni  7323  riotabidva  7336  snriota  7350  oveq  7366  oveq1  7367  oveq2  7368  oprabbid  7425  oprabbidv  7426  mpoeq123  7432  mpoeq123dva  7434  mpoeq3dva  7437  resmpo  7480  ovres  7526  f1ocnvd  7611  ofeqd  7626  ofreq  7628  fpar  8059  frecseq123  8226  csbfrecsg  8228  wrecseq123  8257  csbwrecsg  8262  onovuni  8276  recseq  8307  tfr2a  8328  rdgeq1  8344  rdgeq2  8345  rdgsucmptf  8361  frsucmpt  8371  seqomeq12  8387  seqomsuc  8390  omopthi  8591  eceq1  8677  eceq2  8679  qseq1  8697  qseq2  8698  uniqs  8714  snecg  8718  ecinxp  8733  qsinxp  8734  erovlem  8754  ecopovtrn  8761  ixpeq1  8850  unfi  9099  supeq1  9352  supeq2  9355  supeq3  9356  supeq123d  9357  infeq1  9384  infeq2  9387  infeq3  9388  infeq123d  9389  infiso  9417  oieq1  9421  oieq2  9422  ordtypelem1  9427  inf3lemc  9542  wemapwe  9613  ttrcleq  9625  r1sucg  9688  r1limg  9690  rankprb  9770  karden  9814  djueq12  9823  cardiun  9901  acneq  9960  alephlim  9984  alephsuc  9985  alephfplem2  10022  infpssrlem2  10221  fin23lem34  10263  fin23lem35  10264  zorn2lem1  10413  zorn2lem7  10419  fpwwe2lem5  10553  fpwwe2lem12  10560  addpiord  10802  mulpiord  10803  addpqnq  10856  mulpqnq  10859  addassnq  10876  mulassnq  10877  distrnq  10879  lterpq  10888  ltexnq  10893  ltsrpr  10995  00sr  11017  recexsrlem  11021  mulgt0sr  11023  addcnsrec  11061  mulcnsrec  11062  negeq  11380  csbnegg  11385  negsubdi  11445  mulneg1  11581  negfi  12100  deceq1  12644  deceq2  12645  xnegeq  13154  fseq1p1m1  13547  om2uzrdg  13913  uzrdgsuci  13917  seqeq1  13961  seqeq2  13962  seqeq3  13963  seqfeq4  14008  seqof  14016  hashprg  14352  hashtpg  14442  csbwrdg  14501  s1eq  14558  cats1co  14813  s2eqd  14820  s3eqd  14821  s4eqd  14822  s5eqd  14823  s6eqd  14824  s7eqd  14825  s8eqd  14826  xpcogend  14931  shftval  15031  limsupgle  15434  lo1eq  15525  rlimeq  15526  sumeq1  15646  sumeq2w  15649  sumeq2ii  15650  sumeq2sdv  15660  zsum  15675  sumss2  15683  fsumsplitsnun  15712  isumclim3  15716  fsumcom2  15731  incexclem  15796  incexc2  15798  isumshft  15799  prodeq1f  15866  prodeq1  15867  prodeq2w  15870  prodeq2ii  15871  prodeq2sdv  15883  zprod  15897  fprodm1s  15930  fprodp1s  15931  fprodcom2  15944  fprodsplitf  15948  iprodclim3  15960  ef0lem  16038  ruclem7  16198  sadcp1  16419  smupp1  16444  smueqlem  16454  algrp1  16538  dfphi2  16739  prmdiveq  16751  pceulem  16811  vdwlem6  16952  cshwsiun  17065  sloteq  17148  setsid  17172  elbasfv  17180  elbasov  17181  imastset  17481  imasvscaval  17497  isoval  17727  funcoppc  17837  fulloppc  17886  fuccofval  17924  natpropd  17941  catccofval  18066  xpchomfval  18140  xpccofval  18143  lubfval  18309  glbfval  18322  chneq1  18573  chneq2  18574  grpidpropd  18625  gsumpropd2lem  18642  frmdplusg  18817  efmndplusg  18843  grpinvpropd  18986  grpsubpropd  19016  grpsubpropd2  19017  mulgpropd  19087  ecqusaddd  19162  oppgmnd  19324  sylow1lem2  19569  sylow3lem1  19597  prds1  20297  pwsmgp  20301  opprrng  20320  rngidpropd  20390  dvdsrpropd  20391  unitpropd  20392  invrpropd  20393  rhm1  20464  rhmopp  20485  rhmsubclem2  20662  lmhmpropd  21067  lidlrsppropd  21241  rngqiprnglinlem2  21289  lpival  21321  pzriprnglem11  21470  zrhpropd  21493  znle  21515  frlmplusgval  21743  frlmvscafval  21745  ressascl  21875  asclpropd  21876  aspval2  21877  psrbas  21913  psrplusg  21916  psrmulr  21921  psrvscafval  21927  resspsrbas  21952  ressmplbas2  22006  opsrle  22027  opsrbaslem  22029  vr1val  22181  ressply1add  22218  ressply1mul  22219  ressply1vsca  22220  psrplusgpropd  22224  mplbaspropd  22225  psropprmul  22226  ply1baspropd  22231  ply1plusgpropd  22232  ply1sca2  22242  ply1ascl0  22243  ply1ascl1  22244  subrgvr1  22251  coe1mul2lem2  22258  ply1coe1eq  22290  evls1addd  22361  evls1muld  22362  evls1vsca  22363  rhmply1vr1  22374  rhmply1vsca  22375  mamudi  22390  mamudir  22391  matrcl  22399  oftpos  22439  mattpos1  22443  mdetfval  22573  mdetrlin  22589  mdetrsca  22590  mdetrsca2  22591  mdetrlin2  22594  mdetunilem5  22603  madufval  22624  madugsum  22630  idmatidpmat  22724  cpmidpmat  22860  cncmp  23379  2ndcsep  23446  llyeq  23457  nllyeq  23458  xkouni  23586  hmphindis  23784  xkocnv  23801  ptcmplem2  24040  snclseqg  24103  prdstmdd  24111  ustexsym  24203  ucnextcn  24290  metreslem  24349  comet  24500  nrmmetd  24561  nmpropd  24581  isngp3  24585  ngpds  24591  subgnm  24620  tngnm  24638  idnghm  24730  cnmetdval  24757  cnmpopc  24917  htpyco2  24968  phtpyco2  24979  clsocv  25239  rrxprds  25378  rrxnm  25380  rrxplusgvscavalb  25384  ovolunlem1a  25485  voliunlem3  25541  ioombl1lem4  25550  uniioombllem4  25575  itg11  25680  itgeq1f  25760  itgeq1fOLD  25761  itgeq1  25762  itgeq2  25767  iblss2  25795  itgss  25801  itgeqa  25803  itgfsum  25816  itgsplit  25825  ditgeq1  25837  ditgeq2  25838  ditgeq3  25839  dvcmulf  25934  dvmptfsum  25964  dvcnvrelem2  26007  mdegfval  26049  mdegpropd  26071  deg1propd  26073  plyeq0  26198  coe11  26240  dgrlt  26253  dgradd2  26255  dgrmulc  26258  dvply1  26272  fta1lem  26295  pserulm  26409  rlimcnp2  26952  jensenlem1  26972  basellem5  27070  dchrbas  27220  dchrrcl  27225  dchrplusg  27232  dchrfi  27240  lgsdi  27319  lgseisenlem2  27361  lgsquadlem3  27367  dchrmusumlema  27478  rpvmasum2  27497  dchrisum0lema  27499  pntlemg  27583  nosupbnd2lem1  27701  lruneq  27921  addsval  27976  mulsval  28123  seqseq123d  28300  colperpexlem2  28821  axlowdimlem13  29045  uhgrvtxedgiedgb  29227  nb3grprlem1  29471  crctcshlem2  29908  wpthswwlks2on  30054  clwlknf1oclwwlkn  30176  frgrncvvdeq  30401  avril1  30555  0vfval  30699  imsval  30778  imsdval  30779  bcseqi  31213  normpythi  31235  cm0  31702  fh1  31711  pjcji  31777  opsqrlem5  32237  pjsdi2i  32250  pjclem3  32290  pjci  32293  golem1  32364  iuneq12daf  32649  iunrdx  32656  ofresid  32738  cnvprop  32792  coprprop  32795  f1od2  32815  dp2eq1  32955  dp2eq2  32956  fzto1st1  33187  gsumvsca1  33311  gsumvsca2  33312  urpropd  33316  resv1r  33426  nsgqusf1olem2  33501  oppr2idl  33573  opprqus0g  33577  ressply1evls1  33660  esplyfvn  33773  vietalem  33775  lindsunlem  33820  fedgmullem1  33825  fedgmullem2  33826  fedgmul  33827  fldsdrgfldext2  33858  fldextrspunlem1  33871  fldextrspunfld  33872  algextdeglem4  33916  crefeq  34041  rspectopn  34063  xrge0mulc1cn  34137  qqhval2  34178  esumeq12dvaf  34227  esumeq2  34232  esumf1o  34246  esumfzf  34265  esumss  34268  esumpfinvalf  34272  ofceq  34293  carsgclctunlem1  34513  itgeq12dv  34522  ccatmulgnn0dir  34738  breprexpnat  34830  bnj956  34974  bnj1385  35029  bnj96  35062  bnj548  35094  bnj553  35095  bnj554  35096  bnj602  35112  bnj18eq1  35124  bnj1234  35210  bnj1296  35218  bnj1318  35222  bnj1442  35246  bnj1450  35247  cvmliftlem5  35532  cvmliftlem10  35537  cvmlift2lem9  35554  cvmliftphtlem  35560  satfdm  35612  mthmpps  35825  rdgprc  36035  dfrdg2  36036  wsuceq123  36055  wlimeq12  36060  altopthsn  36204  altxpeq1  36216  altxpeq2  36217  ixpeq12dv  36459  prodeq12sdv  36461  itgeq12sdv  36462  ditgeq123dv  36464  cbvcsbdavw  36502  cbvcsbdavw2  36503  cbvrabdavw  36504  cbviundavw  36505  cbviindavw  36506  cbvopab1davw  36507  cbvopab2davw  36508  cbvopabdavw  36509  cbvmptdavw  36510  cbviotadavw  36512  cbvriotadavw  36513  cbvoprab1davw  36514  cbvoprab2davw  36515  cbvoprab3davw  36516  cbvoprab123davw  36517  cbvoprab12davw  36518  cbvoprab23davw  36519  cbvoprab13davw  36520  cbvixpdavw  36521  cbvsumdavw  36522  cbvproddavw  36523  cbvitgdavw  36524  cbvditgdavw  36525  cbvrabdavw2  36528  cbviundavw2  36529  cbviindavw2  36530  cbvmptdavw2  36531  cbvriotadavw2  36533  cbvmpodavw2  36534  cbvmpo1davw2  36535  cbvmpo2davw2  36536  cbvixpdavw2  36537  cbvsumdavw2  36538  cbvproddavw2  36539  cbvitgdavw2  36540  cbvditgdavw2  36541  ee7.2aOLD  36704  ttceq  36731  bj-sngleq  37335  bj-tageq  37344  bj-projeq  37360  bj-projval  37364  bj-1upleq  37367  bj-pr1eq  37370  bj-pr2eq  37384  bj-evaleq  37444  bj-imafv  37626  csbrecsg  37705  csbrdgg  37706  csboprabg  37707  csbmpo123  37708  finxpeq1  37763  finxpeq2  37764  csbfinxpg  37765  finxpreclem4  37771  cureq  37978  unceq  37979  uncov  37983  unccur  37985  finixpnum  37987  ptrest  38001  poimirlem3  38005  poimirlem9  38011  poimirlem15  38017  poimirlem16  38018  poimirlem26  38028  poimirlem27  38029  mbfposadd  38049  cnambfre  38050  iblabsnclem  38065  ftc1anclem1  38075  heiborlem4  38196  heiborlem6  38198  mpobi123f  38544  iineq12f  38546  mptbi12f  38548  eccnvepres  38668  xrneq1  38778  xrneq2  38781  shiftstableeq2  38865  cosseq  38898  redundss3  39094  riotaclbgBAD  39461  toycom  39480  ldualvbase  39633  ldualfvadd  39635  ldualsca  39639  ldualsbase  39640  ldualsaddN  39641  ldualfvs  39643  ldual0  39654  ldual1  39655  ldualneg  39656  cdleme19f  40815  cdleme20m  40830  cdleme21k  40845  cdleme27b  40875  cdleme31so  40886  cdleme31sn  40887  cdleme31se  40889  cdleme31se2  40890  cdleme31sc  40891  cdleme31sde  40892  cdleme31fv  40897  cdleme40v  40976  cdleme43dN  40999  cdlemeg46ngfr  41025  ltrnco4  41246  tgrpbase  41253  tgrpopr  41254  erngbase  41308  erngfplus  41309  erngfmul  41312  erngbase-rN  41316  erngfplus-rN  41317  erngfmul-rN  41320  dvasca  41513  dvavbase  41520  dvafvadd  41521  dvafvsca  41523  tendocnv  41528  dvhsca  41589  dvhfplusr  41591  dvhvbase  41594  dvhfvadd  41598  dvhfvsca  41607  lcdvadd  42104  lcdsbase  42107  lcdsadd  42108  lcdvs  42110  lcd0  42115  lcd1  42116  lcdneg  42117  fsuppind  43055  imaiinfv  43157  mapfzcons1  43181  rexrabdioph  43254  dnnumch1  43504  dnwech  43508  aomclem6  43519  pwssplit4  43549  pwfi2f1o  43556  mendplusgfval  43641  mendvscafval  43646  harval3  43997  dssmapntrcls  44587  scotteqd  44696  colleq12d  44712  uzmptshftfval  44805  dropab1  44905  dropab2  44906  iineq12dv  45567  rabbida2  45593  rabbida3  45596  itgsinexplem1  46411  wallispi2lem2  46529  fourierdlem36  46600  etransclem4  46695  fcoreslem1  47540  afveq12d  47610  aoveq123d  47655  aovfundmoveq  47658  aovnuoveq  47668  aovvoveq  47669  aovovn0oveq  47671  afv2eq12d  47692  fsumsplitsndif  47858  rngccofvalALTV  48775  rhmsubcALTVlem2  48787  ringccofvalALTV  48809  itscnhlinecirc02plem2  49288  oppfrcl3  49634  oppf1st2nd  49635  uppropd  49685  natoppf  49733  catcrcl  49899  lmdpropd  50161  cmdpropd  50162  lmddu  50171  cmddu  50172  setrecseq  50189  aacllem  50305