Theorem 3eqtr4g 2793

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  rabbidva2  3399  rabbida4  3422  rabeqf  3431  csbeq1  3850  csbeq2  3852  csbeq2d  3853  csbeq2dv  3854  difeq1  4070  difeq2  4071  uneq2  4113  ineq1  4164  ineq2  4165  symdifeq1  4206  symdifeq2  4207  dfrab3ss  4274  csbprc  4360  csbnestgfw  4373  csbnestgf  4378  disjssun  4419  ifeq1  4480  ifeq2  4481  pweqALT  4566  sneq  4587  rabsneq  4596  csbsng  4662  csbprg  4663  preq1  4687  preq2  4688  tpeq1  4696  tpeq2  4697  tpeq3  4698  prprc1  4719  tpprceq3  4757  opeq1  4826  opeq2  4827  oteq1  4835  oteq2  4836  oteq3  4837  csbopg  4844  uniprg  4876  csbuni  4890  inteq  4902  iineq1  4961  iineq2  4964  iuneq12df  4970  iuneq12d  4973  dfiin2g  4983  iinrab  5021  iinin1  5031  iinxprg  5041  iununi  5051  opabbid  5160  opabbidv  5161  mpteq12da  5178  mpteq12f  5180  mpteq12dva  5181  csbmpt12  5502  xpeq1  5635  xpeq2  5642  rneq  5883  reseq1  5929  reseq2  5930  resima2  5972  resindm  5986  resmpt  5993  resmptf  5995  imaeq1  6011  imaeq2  6012  mptcnv  6093  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  7082  residpr  7085  fsnunfv  7130  fsnunres  7131  funiunfv  7191  f1ofvswap  7249  fliftf  7258  isoini2  7282  eqfunressuc  7304  riotaeqdv  7313  riotabidv  7314  riotauni  7318  riotabidva  7331  snriota  7345  oveq  7361  oveq1  7362  oveq2  7363  oprabbid  7420  oprabbidv  7421  mpoeq123  7427  mpoeq123dva  7429  mpoeq3dva  7432  resmpo  7475  ovres  7521  f1ocnvd  7606  ofeqd  7621  ofreq  7623  fpar  8055  frecseq123  8221  csbfrecsg  8223  wrecseq123  8252  csbwrecsg  8257  onovuni  8271  recseq  8302  tfr2a  8323  rdgeq1  8339  rdgeq2  8340  rdgsucmptf  8356  frsucmpt  8366  seqomeq12  8382  seqomsuc  8385  omopthi  8585  eceq1  8670  eceq2  8672  qseq1  8690  qseq2  8691  uniqs  8707  ecinxp  8725  qsinxp  8726  erovlem  8746  ecopovtrn  8753  ixpeq1  8841  unfi  9090  supeq1  9339  supeq2  9342  supeq3  9343  supeq123d  9344  infeq1  9371  infeq2  9374  infeq3  9375  infeq123d  9376  infiso  9404  oieq1  9408  oieq2  9409  ordtypelem1  9414  inf3lemc  9526  wemapwe  9597  ttrcleq  9609  r1sucg  9672  r1limg  9674  rankprb  9754  karden  9798  djueq12  9807  cardiun  9885  acneq  9944  alephlim  9968  alephsuc  9969  alephfplem2  10006  infpssrlem2  10205  fin23lem34  10247  fin23lem35  10248  zorn2lem1  10397  zorn2lem7  10403  fpwwe2lem5  10536  fpwwe2lem12  10543  addpiord  10785  mulpiord  10786  addpqnq  10839  mulpqnq  10842  addassnq  10859  mulassnq  10860  distrnq  10862  lterpq  10871  ltexnq  10876  ltsrpr  10978  00sr  11000  recexsrlem  11004  mulgt0sr  11006  addcnsrec  11044  mulcnsrec  11045  negeq  11362  csbnegg  11367  negsubdi  11427  mulneg1  11563  negfi  12081  deceq1  12603  deceq2  12604  xnegeq  13116  fseq1p1m1  13508  om2uzrdg  13873  uzrdgsuci  13877  seqeq1  13921  seqeq2  13922  seqeq3  13923  seqfeq4  13968  seqof  13976  hashprg  14312  hashtpg  14402  csbwrdg  14461  s1eq  14518  cats1co  14773  s2eqd  14780  s3eqd  14781  s4eqd  14782  s5eqd  14783  s6eqd  14784  s7eqd  14785  s8eqd  14786  xpcogend  14891  shftval  14991  limsupgle  15394  lo1eq  15485  rlimeq  15486  sumeq1  15606  sumeq2w  15609  sumeq2ii  15610  sumeq2sdv  15620  zsum  15635  sumss2  15643  fsumsplitsnun  15672  isumclim3  15676  fsumcom2  15691  incexclem  15753  incexc2  15755  isumshft  15756  prodeq1f  15823  prodeq1  15824  prodeq2w  15827  prodeq2ii  15828  prodeq2sdv  15840  zprod  15854  fprodm1s  15887  fprodp1s  15888  fprodcom2  15901  fprodsplitf  15905  iprodclim3  15917  ef0lem  15995  ruclem7  16155  sadcp1  16376  smupp1  16401  smueqlem  16411  algrp1  16495  dfphi2  16695  prmdiveq  16707  pceulem  16767  vdwlem6  16908  cshwsiun  17021  sloteq  17104  setsid  17128  elbasfv  17136  elbasov  17137  imastset  17436  imasvscaval  17452  isoval  17682  funcoppc  17792  fulloppc  17841  fuccofval  17879  natpropd  17896  catccofval  18021  xpchomfval  18095  xpccofval  18098  lubfval  18264  glbfval  18277  chneq1  18528  chneq2  18529  grpidpropd  18580  gsumpropd2lem  18597  frmdplusg  18772  efmndplusg  18798  grpinvpropd  18938  grpsubpropd  18968  grpsubpropd2  18969  mulgpropd  19039  ecqusaddd  19114  oppgmnd  19276  sylow1lem2  19521  sylow3lem1  19549  prds1  20251  pwsmgp  20255  opprrng  20273  rngidpropd  20343  dvdsrpropd  20344  unitpropd  20345  invrpropd  20346  rhm1  20416  rhmopp  20434  rhmsubclem2  20611  lmhmpropd  21017  lidlrsppropd  21191  rngqiprnglinlem2  21239  lpival  21271  pzriprnglem11  21438  zrhpropd  21461  znle  21483  frlmplusgval  21711  frlmvscafval  21713  ressascl  21843  asclpropd  21844  aspval2  21845  psrbas  21880  psrplusg  21883  psrmulr  21889  psrvscafval  21895  resspsrbas  21921  ressmplbas2  21972  opsrle  21992  opsrbaslem  21994  vr1val  22114  ressply1add  22152  ressply1mul  22153  ressply1vsca  22154  psrplusgpropd  22158  mplbaspropd  22159  psropprmul  22160  ply1baspropd  22165  ply1plusgpropd  22166  ply1sca2  22176  ply1ascl0  22177  ply1ascl1  22178  subrgvr1  22185  coe1mul2lem2  22192  ply1coe1eq  22225  evls1addd  22296  evls1muld  22297  evls1vsca  22298  rhmply1vr1  22312  rhmply1vsca  22313  mamudi  22328  mamudir  22329  matrcl  22337  oftpos  22377  mattpos1  22381  mdetfval  22511  mdetrlin  22527  mdetrsca  22528  mdetrsca2  22529  mdetrlin2  22532  mdetunilem5  22541  madufval  22562  madugsum  22568  idmatidpmat  22662  cpmidpmat  22798  cncmp  23317  2ndcsep  23384  llyeq  23395  nllyeq  23396  xkouni  23524  hmphindis  23722  xkocnv  23739  ptcmplem2  23978  snclseqg  24041  prdstmdd  24049  ustexsym  24141  ucnextcn  24228  metreslem  24287  comet  24438  nrmmetd  24499  nmpropd  24519  isngp3  24523  ngpds  24529  subgnm  24558  tngnm  24576  idnghm  24668  cnmetdval  24695  cnmpopc  24859  htpyco2  24915  phtpyco2  24926  clsocv  25187  rrxprds  25326  rrxnm  25328  rrxplusgvscavalb  25332  ovolunlem1a  25434  voliunlem3  25490  ioombl1lem4  25499  uniioombllem4  25524  itg11  25629  itgeq1f  25709  itgeq1fOLD  25710  itgeq1  25711  itgeq2  25716  iblss2  25744  itgss  25750  itgeqa  25752  itgfsum  25765  itgsplit  25774  ditgeq1  25786  ditgeq2  25787  ditgeq3  25788  dvcmulf  25885  dvmptfsum  25916  dvcnvrelem2  25960  mdegfval  26004  mdegpropd  26026  deg1propd  26028  plyeq0  26153  coe11  26195  dgrlt  26209  dgradd2  26211  dgrmulc  26214  dvply1  26228  fta1lem  26252  pserulm  26368  rlimcnp2  26913  jensenlem1  26934  basellem5  27032  dchrbas  27183  dchrrcl  27188  dchrplusg  27195  dchrfi  27203  lgsdi  27282  lgseisenlem2  27324  lgsquadlem3  27330  dchrmusumlema  27441  rpvmasum2  27460  dchrisum0lema  27462  pntlemg  27546  nosupbnd2lem1  27664  lruneq  27862  addsval  27915  mulsval  28058  seqseq123d  28226  colperpexlem2  28719  axlowdimlem13  28943  uhgrvtxedgiedgb  29125  nb3grprlem1  29369  crctcshlem2  29807  wpthswwlks2on  29953  clwlknf1oclwwlkn  30075  frgrncvvdeq  30300  avril1  30454  0vfval  30597  imsval  30676  imsdval  30677  bcseqi  31111  normpythi  31133  cm0  31600  fh1  31609  pjcji  31675  opsqrlem5  32135  pjsdi2i  32148  pjclem3  32188  pjci  32191  golem1  32262  iuneq12daf  32547  iunrdx  32554  ofresid  32635  cnvprop  32688  coprprop  32691  f1od2  32713  dp2eq1  32864  dp2eq2  32865  fzto1st1  33082  gsumvsca1  33206  gsumvsca2  33207  urpropd  33210  resv1r  33315  nsgqusf1olem2  33390  oppr2idl  33462  opprqus0g  33466  ressply1evls1  33539  lindsunlem  33648  fedgmullem1  33653  fedgmullem2  33654  fedgmul  33655  fldsdrgfldext2  33686  fldextrspunlem1  33699  fldextrspunfld  33700  algextdeglem4  33744  crefeq  33869  rspectopn  33891  xrge0mulc1cn  33965  qqhval2  34006  esumeq12dvaf  34055  esumeq2  34060  esumf1o  34074  esumfzf  34093  esumss  34096  esumpfinvalf  34100  ofceq  34121  carsgclctunlem1  34341  itgeq12dv  34350  ccatmulgnn0dir  34566  breprexpnat  34658  bnj956  34799  bnj1385  34855  bnj96  34888  bnj548  34920  bnj553  34921  bnj554  34922  bnj602  34938  bnj18eq1  34950  bnj1234  35036  bnj1296  35044  bnj1318  35048  bnj1442  35072  bnj1450  35073  cvmliftlem5  35344  cvmliftlem10  35349  cvmlift2lem9  35366  cvmliftphtlem  35372  satfdm  35424  mthmpps  35637  rdgprc  35847  dfrdg2  35848  wsuceq123  35867  wlimeq12  35872  altopthsn  36016  altxpeq1  36028  altxpeq2  36029  ixpeq12dv  36271  prodeq12sdv  36273  itgeq12sdv  36274  ditgeq123dv  36276  cbvcsbdavw  36314  cbvcsbdavw2  36315  cbvrabdavw  36316  cbviundavw  36317  cbviindavw  36318  cbvopab1davw  36319  cbvopab2davw  36320  cbvopabdavw  36321  cbvmptdavw  36322  cbviotadavw  36324  cbvriotadavw  36325  cbvoprab1davw  36326  cbvoprab2davw  36327  cbvoprab3davw  36328  cbvoprab123davw  36329  cbvoprab12davw  36330  cbvoprab23davw  36331  cbvoprab13davw  36332  cbvixpdavw  36333  cbvsumdavw  36334  cbvproddavw  36335  cbvitgdavw  36336  cbvditgdavw  36337  cbvrabdavw2  36340  cbviundavw2  36341  cbviindavw2  36342  cbvmptdavw2  36343  cbvriotadavw2  36345  cbvmpodavw2  36346  cbvmpo1davw2  36347  cbvmpo2davw2  36348  cbvixpdavw2  36349  cbvsumdavw2  36350  cbvproddavw2  36351  cbvitgdavw2  36352  cbvditgdavw2  36353  ee7.2aOLD  36516  bj-sngleq  37022  bj-tageq  37031  bj-projeq  37047  bj-projval  37051  bj-1upleq  37054  bj-pr1eq  37057  bj-pr2eq  37071  bj-evaleq  37127  bj-imafv  37306  csbrecsg  37383  csbrdgg  37384  csboprabg  37385  csbmpo123  37386  finxpeq1  37441  finxpeq2  37442  csbfinxpg  37443  finxpreclem4  37449  cureq  37646  unceq  37647  uncov  37651  unccur  37653  finixpnum  37655  ptrest  37669  poimirlem3  37673  poimirlem9  37679  poimirlem15  37685  poimirlem16  37686  poimirlem26  37696  poimirlem27  37697  mbfposadd  37717  cnambfre  37718  iblabsnclem  37733  ftc1anclem1  37743  heiborlem4  37864  heiborlem6  37866  mpobi123f  38212  iineq12f  38214  mptbi12f  38216  eccnvepres  38328  xrneq1  38430  xrneq2  38433  cosseq  38538  redundss3  38734  riotaclbgBAD  39063  toycom  39082  ldualvbase  39235  ldualfvadd  39237  ldualsca  39241  ldualsbase  39242  ldualsaddN  39243  ldualfvs  39245  ldual0  39256  ldual1  39257  ldualneg  39258  cdleme19f  40417  cdleme20m  40432  cdleme21k  40447  cdleme27b  40477  cdleme31so  40488  cdleme31sn  40489  cdleme31se  40491  cdleme31se2  40492  cdleme31sc  40493  cdleme31sde  40494  cdleme31fv  40499  cdleme40v  40578  cdleme43dN  40601  cdlemeg46ngfr  40627  ltrnco4  40848  tgrpbase  40855  tgrpopr  40856  erngbase  40910  erngfplus  40911  erngfmul  40914  erngbase-rN  40918  erngfplus-rN  40919  erngfmul-rN  40922  dvasca  41115  dvavbase  41122  dvafvadd  41123  dvafvsca  41125  tendocnv  41130  dvhsca  41191  dvhfplusr  41193  dvhvbase  41196  dvhfvadd  41200  dvhfvsca  41209  lcdvadd  41706  lcdsbase  41709  lcdsadd  41710  lcdvs  41712  lcd0  41717  lcd1  41718  lcdneg  41719  fsuppind  42698  imaiinfv  42800  mapfzcons1  42824  rexrabdioph  42901  dnnumch1  43151  dnwech  43155  aomclem6  43166  pwssplit4  43196  pwfi2f1o  43203  mendplusgfval  43288  mendvscafval  43293  harval3  43645  dssmapntrcls  44235  scotteqd  44344  colleq12d  44360  uzmptshftfval  44453  dropab1  44553  dropab2  44554  iineq12dv  45217  rabbida2  45243  rabbida3  45246  itgsinexplem1  46066  wallispi2lem2  46184  fourierdlem36  46255  etransclem4  46350  fcoreslem1  47177  afveq12d  47247  aoveq123d  47292  aovfundmoveq  47295  aovnuoveq  47305  aovvoveq  47306  aovovn0oveq  47308  afv2eq12d  47329  fsumsplitsndif  47487  rngccofvalALTV  48384  rhmsubcALTVlem2  48396  ringccofvalALTV  48418  itscnhlinecirc02plem2  48898  oppfrcl3  49245  oppf1st2nd  49246  uppropd  49296  natoppf  49344  catcrcl  49510  lmdpropd  49772  cmdpropd  49773  lmddu  49782  cmddu  49783  setrecseq  49800  aacllem  49916