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 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 2707

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

This theorem is referenced by:  rabbidva2  3417  rabbida4  3441  rabeqf  3451  csbeq1  3877  csbeq2  3879  csbeq2d  3880  csbeq2dv  3881  difeq1  4094  difeq2  4095  uneq2  4137  ineq1  4188  ineq2  4189  symdifeq1  4230  symdifeq2  4231  dfrab3ss  4298  csbprc  4384  csbnestgfw  4397  csbnestgf  4402  disjssun  4443  ifeq1  4504  ifeq2  4505  pweqALT  4590  sneq  4611  rabsneq  4620  csbsng  4684  csbprg  4685  preq1  4709  preq2  4710  tpeq1  4718  tpeq2  4719  tpeq3  4720  prprc1  4741  tpprceq3  4780  opeq1  4849  opeq2  4850  oteq1  4858  oteq2  4859  oteq3  4860  csbopg  4867  uniprg  4899  csbuni  4912  inteq  4925  iineq1  4985  iineq2  4988  iuneq12df  4994  iuneq12d  4997  dfiin2g  5008  iinrab  5045  iinin1  5055  iinxprg  5065  iununi  5075  opabbid  5184  opabbidv  5185  mpteq12da  5203  mpteq12f  5205  mpteq12dva  5206  csbmpt12  5532  xpeq1  5668  xpeq2  5675  rneq  5916  reseq1  5960  reseq2  5961  resima2  6003  resindm  6017  resmpt  6024  resmptf  6026  imaeq1  6042  imaeq2  6043  mptcnv  6128  xpdisj1  6150  xpdisj2  6151  resdisj  6158  dmpropg  6204  rnpropg  6211  cores  6238  cores2  6248  xpco  6278  predeq123  6291  csbpredg  6296  sspred  6299  predres  6328  suceq  6419  sucprc  6429  iotaeq  6495  iotabi  6496  fntpg  6595  imain  6620  f1oprswap  6861  fveq1  6874  fveq2  6875  fvres  6894  csbfv12  6923  fnimapr  6961  fnimatpd  6962  fvco2  6975  xpprsng  7129  residpr  7132  fsnunfv  7178  fsnunres  7179  funiunfv  7239  f1ofvswap  7298  fliftf  7307  isoini2  7331  eqfunressuc  7353  riotaeqdv  7361  riotabidv  7362  riotauni  7366  riotabidva  7379  snriota  7393  oveq  7409  oveq1  7410  oveq2  7411  oprabbid  7470  oprabbidv  7471  mpoeq123  7477  mpoeq123dva  7479  mpoeq3dva  7482  resmpo  7525  ovres  7571  f1ocnvd  7656  ofeqd  7671  ofreq  7673  fpar  8113  frecseq123  8279  csbfrecsg  8281  wrecseq123  8311  wrecseq123OLD  8312  csbwrecsg  8318  onovuni  8354  recseq  8386  tfr2a  8407  rdgeq1  8423  rdgeq2  8424  rdgsucmptf  8440  frsucmpt  8450  seqomeq12  8466  seqomsuc  8469  omopthi  8671  eceq1  8756  eceq2  8758  qseq1  8773  qseq2  8774  uniqs  8789  ecinxp  8804  qsinxp  8805  erovlem  8825  ecopovtrn  8832  ixpeq1  8920  unfi  9183  supeq1  9455  supeq2  9458  supeq3  9459  supeq123d  9460  infeq1  9487  infeq2  9490  infeq3  9491  infeq123d  9492  infiso  9520  oieq1  9524  oieq2  9525  ordtypelem1  9530  inf3lemc  9638  wemapwe  9709  ttrcleq  9721  r1sucg  9781  r1limg  9783  rankprb  9863  karden  9907  djueq12  9916  cardiun  9994  acneq  10055  alephlim  10079  alephsuc  10080  alephfplem2  10117  infpssrlem2  10316  fin23lem34  10358  fin23lem35  10359  zorn2lem1  10508  zorn2lem7  10514  fpwwe2lem5  10647  fpwwe2lem12  10654  addpiord  10896  mulpiord  10897  addpqnq  10950  mulpqnq  10953  addassnq  10970  mulassnq  10971  distrnq  10973  lterpq  10982  ltexnq  10987  ltsrpr  11089  00sr  11111  recexsrlem  11115  mulgt0sr  11117  addcnsrec  11155  mulcnsrec  11156  negeq  11472  csbnegg  11477  negsubdi  11537  mulneg1  11671  negfi  12189  deceq1  12711  deceq2  12712  xnegeq  13221  fseq1p1m1  13613  om2uzrdg  13972  uzrdgsuci  13976  seqeq1  14020  seqeq2  14021  seqeq3  14022  seqfeq4  14067  seqof  14075  hashprg  14411  hashtpg  14501  csbwrdg  14560  s1eq  14616  cats1co  14873  s2eqd  14880  s3eqd  14881  s4eqd  14882  s5eqd  14883  s6eqd  14884  s7eqd  14885  s8eqd  14886  xpcogend  14991  shftval  15091  limsupgle  15491  lo1eq  15582  rlimeq  15583  sumeq1  15703  sumeq2w  15706  sumeq2ii  15707  sumeq2sdv  15717  zsum  15732  sumss2  15740  fsumsplitsnun  15769  isumclim3  15773  fsumcom2  15788  incexclem  15850  incexc2  15852  isumshft  15853  prodeq1f  15920  prodeq1  15921  prodeq2w  15924  prodeq2ii  15925  prodeq2sdv  15937  zprod  15951  fprodm1s  15984  fprodp1s  15985  fprodcom2  15998  fprodsplitf  16002  iprodclim3  16014  ef0lem  16092  ruclem7  16252  sadcp1  16472  smupp1  16497  smueqlem  16507  algrp1  16591  dfphi2  16791  prmdiveq  16803  pceulem  16863  vdwlem6  17004  cshwsiun  17117  sloteq  17200  setsid  17224  elbasfv  17232  elbasov  17233  imastset  17534  imasvscaval  17550  isoval  17776  funcoppc  17886  fulloppc  17935  fuccofval  17973  natpropd  17990  catccofval  18115  xpchomfval  18189  xpccofval  18192  lubfval  18358  glbfval  18371  grpidpropd  18638  gsumpropd2lem  18655  frmdplusg  18830  efmndplusg  18856  grpinvpropd  18996  grpsubpropd  19026  grpsubpropd2  19027  mulgpropd  19097  ecqusaddd  19173  oppgmnd  19335  sylow1lem2  19578  sylow3lem1  19606  prds1  20281  pwsmgp  20285  opprrng  20303  rngidpropd  20373  dvdsrpropd  20374  unitpropd  20375  invrpropd  20376  rhm1  20447  rhmopp  20467  rhmsubclem2  20644  lmhmpropd  21029  lidlrsppropd  21203  rngqiprnglinlem2  21251  lpival  21283  pzriprnglem11  21450  zrhpropd  21473  znle  21495  frlmplusgval  21722  frlmvscafval  21724  ressascl  21854  asclpropd  21855  aspval2  21856  psrbas  21891  psrplusg  21894  psrmulr  21900  psrvscafval  21906  resspsrbas  21932  ressmplbas2  21983  opsrle  22003  opsrbaslem  22005  vr1val  22125  ressply1add  22163  ressply1mul  22164  ressply1vsca  22165  psrplusgpropd  22169  mplbaspropd  22170  psropprmul  22171  ply1baspropd  22176  ply1plusgpropd  22177  ply1sca2  22187  ply1ascl0  22188  ply1ascl1  22189  subrgvr1  22196  coe1mul2lem2  22203  ply1coe1eq  22236  evls1addd  22307  evls1muld  22308  evls1vsca  22309  rhmply1vr1  22323  rhmply1vsca  22324  mamudi  22339  mamudir  22340  matrcl  22348  oftpos  22388  mattpos1  22392  mdetfval  22522  mdetrlin  22538  mdetrsca  22539  mdetrsca2  22540  mdetrlin2  22543  mdetunilem5  22552  madufval  22573  madugsum  22579  idmatidpmat  22673  cpmidpmat  22809  cncmp  23328  2ndcsep  23395  llyeq  23406  nllyeq  23407  xkouni  23535  hmphindis  23733  xkocnv  23750  ptcmplem2  23989  snclseqg  24052  prdstmdd  24060  ustexsym  24152  ucnextcn  24240  metreslem  24299  comet  24450  nrmmetd  24511  nmpropd  24531  isngp3  24535  ngpds  24541  subgnm  24570  tngnm  24588  idnghm  24680  cnmetdval  24707  cnmpopc  24871  htpyco2  24927  phtpyco2  24938  clsocv  25200  rrxprds  25339  rrxnm  25341  rrxplusgvscavalb  25345  ovolunlem1a  25447  voliunlem3  25503  ioombl1lem4  25512  uniioombllem4  25537  itg11  25642  itgeq1f  25722  itgeq1fOLD  25723  itgeq1  25724  itgeq2  25729  iblss2  25757  itgss  25763  itgeqa  25765  itgfsum  25778  itgsplit  25787  ditgeq1  25799  ditgeq2  25800  ditgeq3  25801  dvcmulf  25898  dvmptfsum  25929  dvcnvrelem2  25973  mdegfval  26017  mdegpropd  26039  deg1propd  26041  plyeq0  26166  coe11  26208  dgrlt  26222  dgradd2  26224  dgrmulc  26227  dvply1  26241  fta1lem  26265  pserulm  26381  rlimcnp2  26926  jensenlem1  26947  basellem5  27045  dchrbas  27196  dchrrcl  27201  dchrplusg  27208  dchrfi  27216  lgsdi  27295  lgseisenlem2  27337  lgsquadlem3  27343  dchrmusumlema  27454  rpvmasum2  27473  dchrisum0lema  27475  pntlemg  27559  nosupbnd2lem1  27677  lruneq  27861  addsval  27912  mulsval  28052  seqseq123d  28209  colperpexlem2  28656  axlowdimlem13  28879  uhgrvtxedgiedgb  29061  nb3grprlem1  29305  crctcshlem2  29746  wpthswwlks2on  29889  clwlknf1oclwwlkn  30011  frgrncvvdeq  30236  avril1  30390  0vfval  30533  imsval  30612  imsdval  30613  bcseqi  31047  normpythi  31069  cm0  31536  fh1  31545  pjcji  31611  opsqrlem5  32071  pjsdi2i  32084  pjclem3  32124  pjci  32127  golem1  32198  iuneq12daf  32483  iunrdx  32490  ofresid  32566  cnvprop  32619  coprprop  32622  f1od2  32644  dp2eq1  32793  dp2eq2  32794  fzto1st1  33059  gsumvsca1  33169  gsumvsca2  33170  urpropd  33173  resv1r  33301  nsgqusf1olem2  33375  oppr2idl  33447  opprqus0g  33451  ressply1evls1  33524  lindsunlem  33610  fedgmullem1  33615  fedgmullem2  33616  fedgmul  33617  fldsdrgfldext2  33650  fldextrspunlem1  33662  fldextrspunfld  33663  algextdeglem4  33700  crefeq  33822  rspectopn  33844  xrge0mulc1cn  33918  qqhval2  33959  esumeq12dvaf  34008  esumeq2  34013  esumf1o  34027  esumfzf  34046  esumss  34049  esumpfinvalf  34053  ofceq  34074  carsgclctunlem1  34295  itgeq12dv  34304  ccatmulgnn0dir  34520  breprexpnat  34612  bnj956  34753  bnj1385  34809  bnj96  34842  bnj548  34874  bnj553  34875  bnj554  34876  bnj602  34892  bnj18eq1  34904  bnj1234  34990  bnj1296  34998  bnj1318  35002  bnj1442  35026  bnj1450  35027  cvmliftlem5  35257  cvmliftlem10  35262  cvmlift2lem9  35279  cvmliftphtlem  35285  satfdm  35337  mthmpps  35550  rdgprc  35758  dfrdg2  35759  wsuceq123  35778  wlimeq12  35783  altopthsn  35925  altxpeq1  35937  altxpeq2  35938  ixpeq12dv  36180  prodeq12sdv  36182  itgeq12sdv  36183  ditgeq123dv  36185  cbvcsbdavw  36223  cbvcsbdavw2  36224  cbvrabdavw  36225  cbviundavw  36226  cbviindavw  36227  cbvopab1davw  36228  cbvopab2davw  36229  cbvopabdavw  36230  cbvmptdavw  36231  cbviotadavw  36233  cbvriotadavw  36234  cbvoprab1davw  36235  cbvoprab2davw  36236  cbvoprab3davw  36237  cbvoprab123davw  36238  cbvoprab12davw  36239  cbvoprab23davw  36240  cbvoprab13davw  36241  cbvixpdavw  36242  cbvsumdavw  36243  cbvproddavw  36244  cbvitgdavw  36245  cbvditgdavw  36246  cbvrabdavw2  36249  cbviundavw2  36250  cbviindavw2  36251  cbvmptdavw2  36252  cbvriotadavw2  36254  cbvmpodavw2  36255  cbvmpo1davw2  36256  cbvmpo2davw2  36257  cbvixpdavw2  36258  cbvsumdavw2  36259  cbvproddavw2  36260  cbvitgdavw2  36261  cbvditgdavw2  36262  ee7.2aOLD  36425  bj-sngleq  36931  bj-tageq  36940  bj-projeq  36956  bj-projval  36960  bj-1upleq  36963  bj-pr1eq  36966  bj-pr2eq  36980  bj-evaleq  37036  bj-imafv  37215  csbrecsg  37292  csbrdgg  37293  csboprabg  37294  csbmpo123  37295  finxpeq1  37350  finxpeq2  37351  csbfinxpg  37352  finxpreclem4  37358  cureq  37566  unceq  37567  uncov  37571  unccur  37573  finixpnum  37575  ptrest  37589  poimirlem3  37593  poimirlem9  37599  poimirlem15  37605  poimirlem16  37606  poimirlem26  37616  poimirlem27  37617  mbfposadd  37637  cnambfre  37638  iblabsnclem  37653  ftc1anclem1  37663  heiborlem4  37784  heiborlem6  37786  mpobi123f  38132  iineq12f  38134  mptbi12f  38136  eccnvepres  38244  uniqsALTV  38293  xrneq1  38341  xrneq2  38344  cosseq  38390  redundss3  38592  riotaclbgBAD  38918  toycom  38937  ldualvbase  39090  ldualfvadd  39092  ldualsca  39096  ldualsbase  39097  ldualsaddN  39098  ldualfvs  39100  ldual0  39111  ldual1  39112  ldualneg  39113  cdleme19f  40273  cdleme20m  40288  cdleme21k  40303  cdleme27b  40333  cdleme31so  40344  cdleme31sn  40345  cdleme31se  40347  cdleme31se2  40348  cdleme31sc  40349  cdleme31sde  40350  cdleme31fv  40355  cdleme40v  40434  cdleme43dN  40457  cdlemeg46ngfr  40483  ltrnco4  40704  tgrpbase  40711  tgrpopr  40712  erngbase  40766  erngfplus  40767  erngfmul  40770  erngbase-rN  40774  erngfplus-rN  40775  erngfmul-rN  40778  dvasca  40971  dvavbase  40978  dvafvadd  40979  dvafvsca  40981  tendocnv  40986  dvhsca  41047  dvhfplusr  41049  dvhvbase  41052  dvhfvadd  41056  dvhfvsca  41065  lcdvadd  41562  lcdsbase  41565  lcdsadd  41566  lcdvs  41568  lcd0  41573  lcd1  41574  lcdneg  41575  fsuppind  42560  imaiinfv  42663  mapfzcons1  42687  rexrabdioph  42764  dnnumch1  43015  dnwech  43019  aomclem6  43030  pwssplit4  43060  pwfi2f1o  43067  mendplusgfval  43152  mendvscafval  43157  harval3  43509  dssmapntrcls  44099  scotteqd  44209  colleq12d  44225  uzmptshftfval  44318  dropab1  44419  dropab2  44420  iineq12dv  45078  rabbida2  45104  rabbida3  45107  itgsinexplem1  45931  wallispi2lem2  46049  fourierdlem36  46120  etransclem4  46215  fcoreslem1  47040  afveq12d  47110  aoveq123d  47155  aovfundmoveq  47158  aovnuoveq  47168  aovvoveq  47169  aovovn0oveq  47171  afv2eq12d  47192  fsumsplitsndif  47335  rngccofvalALTV  48193  rhmsubcALTVlem2  48205  ringccofvalALTV  48227  itscnhlinecirc02plem2  48711  oppfrcl3  49026  oppf1st2nd  49027  setrecseq  49497  aacllem  49613