Theorem 3eqtr4g 2797

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

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

This theorem is referenced by:  rabbidva2  3392  rabbida4  3415  csbeq1  3841  csbeq2  3843  csbeq2d  3844  csbeq2dv  3845  difeq1  4060  difeq2  4061  uneq2  4103  ineq1  4154  ineq2  4155  symdifeq1  4196  symdifeq2  4197  dfrab3ss  4264  csbprc  4350  csbnestgfw  4363  csbnestgf  4368  disjssun  4409  ifeq1  4471  ifeq2  4472  pweqALT  4557  sneq  4578  csbsng  4653  csbprg  4654  preq1  4678  preq2  4679  tpeq1  4687  tpeq2  4688  tpeq3  4689  prprc1  4710  tpprceq3  4748  opeq1  4817  opeq2  4818  oteq1  4826  oteq2  4827  oteq3  4828  csbopg  4835  uniprg  4867  csbuni  4881  inteq  4893  iineq1  4952  iineq2  4955  iuneq12df  4961  iuneq12d  4964  dfiin2g  4974  iinrab  5012  iinin1  5022  iinxprg  5032  iununi  5042  opabbid  5151  opabbidv  5152  mpteq12da  5169  mpteq12f  5171  mpteq12dva  5172  csbmpt12  5507  xpeq1  5640  xpeq2  5647  rneq  5887  reseq1  5934  reseq2  5935  resima2  5977  resindm  5991  resmpt  5998  resmptf  6000  imaeq1  6016  imaeq2  6017  mptcnv  6098  xpdisj1  6121  xpdisj2  6122  resdisj  6129  dmpropg  6175  rnpropg  6182  cores  6209  cores2  6220  xpco  6249  predeq123  6262  csbpredg  6267  sspred  6270  predres  6299  suceqd  6386  sucprc  6397  iotaeq  6462  iotabi  6463  fntpg  6554  imain  6579  f1oprswap  6821  fveq1  6835  fveq2  6836  fvres  6855  csbfv12  6881  fnimapr  6919  fnimatpd  6920  fvco2  6933  xpprsng  7089  residpr  7092  fsnunfv  7137  fsnunres  7138  funiunfv  7198  f1ofvswap  7256  fliftf  7265  isoini2  7289  eqfunressuc  7311  riotaeqdv  7320  riotabidv  7321  riotauni  7325  riotabidva  7338  snriota  7352  oveq  7368  oveq1  7369  oveq2  7370  oprabbid  7427  oprabbidv  7428  mpoeq123  7434  mpoeq123dva  7436  mpoeq3dva  7439  resmpo  7482  ovres  7528  f1ocnvd  7613  ofeqd  7628  ofreq  7630  fpar  8061  frecseq123  8227  csbfrecsg  8229  wrecseq123  8258  csbwrecsg  8263  onovuni  8277  recseq  8308  tfr2a  8329  rdgeq1  8345  rdgeq2  8346  rdgsucmptf  8362  frsucmpt  8372  seqomeq12  8388  seqomsuc  8391  omopthi  8592  eceq1  8678  eceq2  8680  qseq1  8698  qseq2  8699  uniqs  8715  snecg  8719  ecinxp  8734  qsinxp  8735  erovlem  8755  ecopovtrn  8762  ixpeq1  8851  unfi  9100  supeq1  9353  supeq2  9356  supeq3  9357  supeq123d  9358  infeq1  9385  infeq2  9388  infeq3  9389  infeq123d  9390  infiso  9418  oieq1  9422  oieq2  9423  ordtypelem1  9428  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  20463  rhmopp  20481  rhmsubclem2  20658  lmhmpropd  21064  lidlrsppropd  21238  rngqiprnglinlem2  21286  lpival  21318  pzriprnglem11  21485  zrhpropd  21508  znle  21530  frlmplusgval  21758  frlmvscafval  21760  ressascl  21890  asclpropd  21891  aspval2  21892  psrbas  21927  psrplusg  21930  psrmulr  21935  psrvscafval  21941  resspsrbas  21966  ressmplbas2  22019  opsrle  22039  opsrbaslem  22041  vr1val  22169  ressply1add  22207  ressply1mul  22208  ressply1vsca  22209  psrplusgpropd  22213  mplbaspropd  22214  psropprmul  22215  ply1baspropd  22220  ply1plusgpropd  22221  ply1sca2  22231  ply1ascl0  22232  ply1ascl1  22233  subrgvr1  22240  coe1mul2lem2  22247  ply1coe1eq  22279  evls1addd  22350  evls1muld  22351  evls1vsca  22352  rhmply1vr1  22366  rhmply1vsca  22367  mamudi  22382  mamudir  22383  matrcl  22391  oftpos  22431  mattpos1  22435  mdetfval  22565  mdetrlin  22581  mdetrsca  22582  mdetrsca2  22583  mdetrlin2  22586  mdetunilem5  22595  madufval  22616  madugsum  22622  idmatidpmat  22716  cpmidpmat  22852  cncmp  23371  2ndcsep  23438  llyeq  23449  nllyeq  23450  xkouni  23578  hmphindis  23776  xkocnv  23793  ptcmplem2  24032  snclseqg  24095  prdstmdd  24103  ustexsym  24195  ucnextcn  24282  metreslem  24341  comet  24492  nrmmetd  24553  nmpropd  24573  isngp3  24577  ngpds  24583  subgnm  24612  tngnm  24630  idnghm  24722  cnmetdval  24749  cnmpopc  24909  htpyco2  24960  phtpyco2  24971  clsocv  25231  rrxprds  25370  rrxnm  25372  rrxplusgvscavalb  25376  ovolunlem1a  25477  voliunlem3  25533  ioombl1lem4  25542  uniioombllem4  25567  itg11  25672  itgeq1f  25752  itgeq1fOLD  25753  itgeq1  25754  itgeq2  25759  iblss2  25787  itgss  25793  itgeqa  25795  itgfsum  25808  itgsplit  25817  ditgeq1  25829  ditgeq2  25830  ditgeq3  25831  dvcmulf  25926  dvmptfsum  25956  dvcnvrelem2  25999  mdegfval  26041  mdegpropd  26063  deg1propd  26065  plyeq0  26190  coe11  26232  dgrlt  26245  dgradd2  26247  dgrmulc  26250  dvply1  26264  fta1lem  26288  pserulm  26404  rlimcnp2  26947  jensenlem1  26968  basellem5  27066  dchrbas  27216  dchrrcl  27221  dchrplusg  27228  dchrfi  27236  lgsdi  27315  lgseisenlem2  27357  lgsquadlem3  27363  dchrmusumlema  27474  rpvmasum2  27493  dchrisum0lema  27495  pntlemg  27579  nosupbnd2lem1  27697  lruneq  27917  addsval  27972  mulsval  28119  seqseq123d  28296  colperpexlem2  28817  axlowdimlem13  29041  uhgrvtxedgiedgb  29223  nb3grprlem1  29467  crctcshlem2  29905  wpthswwlks2on  30051  clwlknf1oclwwlkn  30173  frgrncvvdeq  30398  avril1  30552  0vfval  30696  imsval  30775  imsdval  30776  bcseqi  31210  normpythi  31232  cm0  31699  fh1  31708  pjcji  31774  opsqrlem5  32234  pjsdi2i  32247  pjclem3  32287  pjci  32290  golem1  32361  iuneq12daf  32645  iunrdx  32652  ofresid  32734  cnvprop  32788  coprprop  32791  f1od2  32811  dp2eq1  32951  dp2eq2  32952  fzto1st1  33182  gsumvsca1  33306  gsumvsca2  33307  urpropd  33311  resv1r  33418  nsgqusf1olem2  33493  oppr2idl  33565  opprqus0g  33569  ressply1evls1  33644  esplyfvn  33740  vietalem  33742  lindsunlem  33788  fedgmullem1  33793  fedgmullem2  33794  fedgmul  33795  fldsdrgfldext2  33826  fldextrspunlem1  33839  fldextrspunfld  33840  algextdeglem4  33884  crefeq  34009  rspectopn  34031  xrge0mulc1cn  34105  qqhval2  34146  esumeq12dvaf  34195  esumeq2  34200  esumf1o  34214  esumfzf  34233  esumss  34236  esumpfinvalf  34240  ofceq  34261  carsgclctunlem1  34481  itgeq12dv  34490  ccatmulgnn0dir  34706  breprexpnat  34798  bnj956  34939  bnj1385  34994  bnj96  35027  bnj548  35059  bnj553  35060  bnj554  35061  bnj602  35077  bnj18eq1  35089  bnj1234  35175  bnj1296  35183  bnj1318  35187  bnj1442  35211  bnj1450  35212  cvmliftlem5  35491  cvmliftlem10  35496  cvmlift2lem9  35513  cvmliftphtlem  35519  satfdm  35571  mthmpps  35784  rdgprc  35994  dfrdg2  35995  wsuceq123  36014  wlimeq12  36019  altopthsn  36163  altxpeq1  36175  altxpeq2  36176  ixpeq12dv  36418  prodeq12sdv  36420  itgeq12sdv  36421  ditgeq123dv  36423  cbvcsbdavw  36461  cbvcsbdavw2  36462  cbvrabdavw  36463  cbviundavw  36464  cbviindavw  36465  cbvopab1davw  36466  cbvopab2davw  36467  cbvopabdavw  36468  cbvmptdavw  36469  cbviotadavw  36471  cbvriotadavw  36472  cbvoprab1davw  36473  cbvoprab2davw  36474  cbvoprab3davw  36475  cbvoprab123davw  36476  cbvoprab12davw  36477  cbvoprab23davw  36478  cbvoprab13davw  36479  cbvixpdavw  36480  cbvsumdavw  36481  cbvproddavw  36482  cbvitgdavw  36483  cbvditgdavw  36484  cbvrabdavw2  36487  cbviundavw2  36488  cbviindavw2  36489  cbvmptdavw2  36490  cbvriotadavw2  36492  cbvmpodavw2  36493  cbvmpo1davw2  36494  cbvmpo2davw2  36495  cbvixpdavw2  36496  cbvsumdavw2  36497  cbvproddavw2  36498  cbvitgdavw2  36499  cbvditgdavw2  36500  ee7.2aOLD  36663  ttceq  36690  bj-sngleq  37294  bj-tageq  37303  bj-projeq  37319  bj-projval  37323  bj-1upleq  37326  bj-pr1eq  37329  bj-pr2eq  37343  bj-evaleq  37403  bj-imafv  37585  csbrecsg  37664  csbrdgg  37665  csboprabg  37666  csbmpo123  37667  finxpeq1  37722  finxpeq2  37723  csbfinxpg  37724  finxpreclem4  37730  cureq  37937  unceq  37938  uncov  37942  unccur  37944  finixpnum  37946  ptrest  37960  poimirlem3  37964  poimirlem9  37970  poimirlem15  37976  poimirlem16  37977  poimirlem26  37987  poimirlem27  37988  mbfposadd  38008  cnambfre  38009  iblabsnclem  38024  ftc1anclem1  38034  heiborlem4  38155  heiborlem6  38157  mpobi123f  38503  iineq12f  38505  mptbi12f  38507  eccnvepres  38627  xrneq1  38737  xrneq2  38740  shiftstableeq2  38824  cosseq  38857  redundss3  39053  riotaclbgBAD  39420  toycom  39439  ldualvbase  39592  ldualfvadd  39594  ldualsca  39598  ldualsbase  39599  ldualsaddN  39600  ldualfvs  39602  ldual0  39613  ldual1  39614  ldualneg  39615  cdleme19f  40774  cdleme20m  40789  cdleme21k  40804  cdleme27b  40834  cdleme31so  40845  cdleme31sn  40846  cdleme31se  40848  cdleme31se2  40849  cdleme31sc  40850  cdleme31sde  40851  cdleme31fv  40856  cdleme40v  40935  cdleme43dN  40958  cdlemeg46ngfr  40984  ltrnco4  41205  tgrpbase  41212  tgrpopr  41213  erngbase  41267  erngfplus  41268  erngfmul  41271  erngbase-rN  41275  erngfplus-rN  41276  erngfmul-rN  41279  dvasca  41472  dvavbase  41479  dvafvadd  41480  dvafvsca  41482  tendocnv  41487  dvhsca  41548  dvhfplusr  41550  dvhvbase  41553  dvhfvadd  41557  dvhfvsca  41566  lcdvadd  42063  lcdsbase  42066  lcdsadd  42067  lcdvs  42069  lcd0  42074  lcd1  42075  lcdneg  42076  fsuppind  43043  imaiinfv  43145  mapfzcons1  43169  rexrabdioph  43246  dnnumch1  43496  dnwech  43500  aomclem6  43511  pwssplit4  43541  pwfi2f1o  43548  mendplusgfval  43633  mendvscafval  43638  harval3  43989  dssmapntrcls  44579  scotteqd  44688  colleq12d  44704  uzmptshftfval  44797  dropab1  44897  dropab2  44898  iineq12dv  45560  rabbida2  45586  rabbida3  45589  itgsinexplem1  46406  wallispi2lem2  46524  fourierdlem36  46595  etransclem4  46690  fcoreslem1  47529  afveq12d  47599  aoveq123d  47644  aovfundmoveq  47647  aovnuoveq  47657  aovvoveq  47658  aovovn0oveq  47660  afv2eq12d  47681  fsumsplitsndif  47847  rngccofvalALTV  48764  rhmsubcALTVlem2  48776  ringccofvalALTV  48798  itscnhlinecirc02plem2  49277  oppfrcl3  49623  oppf1st2nd  49624  uppropd  49674  natoppf  49722  catcrcl  49888  lmdpropd  50150  cmdpropd  50151  lmddu  50160  cmddu  50161  setrecseq  50178  aacllem  50294