Theorem 3eqtr4g 2791

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 2778	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2784	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 2121  ax-ext 2703

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

This theorem is referenced by:  rabbidva2  3397  rabbida4  3420  rabeqf  3429  csbeq1  3848  csbeq2  3850  csbeq2d  3851  csbeq2dv  3852  difeq1  4066  difeq2  4067  uneq2  4109  ineq1  4160  ineq2  4161  symdifeq1  4202  symdifeq2  4203  dfrab3ss  4270  csbprc  4356  csbnestgfw  4369  csbnestgf  4374  disjssun  4415  ifeq1  4476  ifeq2  4477  pweqALT  4562  sneq  4583  rabsneq  4592  csbsng  4658  csbprg  4659  preq1  4683  preq2  4684  tpeq1  4692  tpeq2  4693  tpeq3  4694  prprc1  4715  tpprceq3  4753  opeq1  4822  opeq2  4823  oteq1  4831  oteq2  4832  oteq3  4833  csbopg  4840  uniprg  4872  csbuni  4886  inteq  4898  iineq1  4957  iineq2  4960  iuneq12df  4966  iuneq12d  4969  dfiin2g  4979  iinrab  5015  iinin1  5025  iinxprg  5035  iununi  5045  opabbid  5154  opabbidv  5155  mpteq12da  5172  mpteq12f  5174  mpteq12dva  5175  csbmpt12  5495  xpeq1  5628  xpeq2  5635  rneq  5875  reseq1  5921  reseq2  5922  resima2  5964  resindm  5978  resmpt  5985  resmptf  5987  imaeq1  6003  imaeq2  6004  mptcnv  6085  xpdisj1  6108  xpdisj2  6109  resdisj  6116  dmpropg  6162  rnpropg  6169  cores  6196  cores2  6207  xpco  6236  predeq123  6249  csbpredg  6254  sspred  6257  predres  6286  suceqd  6373  sucprc  6384  iotaeq  6449  iotabi  6450  fntpg  6541  imain  6566  f1oprswap  6807  fveq1  6821  fveq2  6822  fvres  6841  csbfv12  6867  fnimapr  6905  fnimatpd  6906  fvco2  6919  xpprsng  7073  residpr  7076  fsnunfv  7121  fsnunres  7122  funiunfv  7182  f1ofvswap  7240  fliftf  7249  isoini2  7273  eqfunressuc  7295  riotaeqdv  7304  riotabidv  7305  riotauni  7309  riotabidva  7322  snriota  7336  oveq  7352  oveq1  7353  oveq2  7354  oprabbid  7411  oprabbidv  7412  mpoeq123  7418  mpoeq123dva  7420  mpoeq3dva  7423  resmpo  7466  ovres  7512  f1ocnvd  7597  ofeqd  7612  ofreq  7614  fpar  8046  frecseq123  8212  csbfrecsg  8214  wrecseq123  8243  csbwrecsg  8248  onovuni  8262  recseq  8293  tfr2a  8314  rdgeq1  8330  rdgeq2  8331  rdgsucmptf  8347  frsucmpt  8357  seqomeq12  8373  seqomsuc  8376  omopthi  8576  eceq1  8661  eceq2  8663  qseq1  8681  qseq2  8682  uniqs  8698  ecinxp  8716  qsinxp  8717  erovlem  8737  ecopovtrn  8744  ixpeq1  8832  unfi  9080  supeq1  9329  supeq2  9332  supeq3  9333  supeq123d  9334  infeq1  9361  infeq2  9364  infeq3  9365  infeq123d  9366  infiso  9394  oieq1  9398  oieq2  9399  ordtypelem1  9404  inf3lemc  9516  wemapwe  9587  ttrcleq  9599  r1sucg  9662  r1limg  9664  rankprb  9744  karden  9788  djueq12  9797  cardiun  9875  acneq  9934  alephlim  9958  alephsuc  9959  alephfplem2  9996  infpssrlem2  10195  fin23lem34  10237  fin23lem35  10238  zorn2lem1  10387  zorn2lem7  10393  fpwwe2lem5  10526  fpwwe2lem12  10533  addpiord  10775  mulpiord  10776  addpqnq  10829  mulpqnq  10832  addassnq  10849  mulassnq  10850  distrnq  10852  lterpq  10861  ltexnq  10866  ltsrpr  10968  00sr  10990  recexsrlem  10994  mulgt0sr  10996  addcnsrec  11034  mulcnsrec  11035  negeq  11352  csbnegg  11357  negsubdi  11417  mulneg1  11553  negfi  12071  deceq1  12593  deceq2  12594  xnegeq  13106  fseq1p1m1  13498  om2uzrdg  13863  uzrdgsuci  13867  seqeq1  13911  seqeq2  13912  seqeq3  13913  seqfeq4  13958  seqof  13966  hashprg  14302  hashtpg  14392  csbwrdg  14451  s1eq  14508  cats1co  14763  s2eqd  14770  s3eqd  14771  s4eqd  14772  s5eqd  14773  s6eqd  14774  s7eqd  14775  s8eqd  14776  xpcogend  14881  shftval  14981  limsupgle  15384  lo1eq  15475  rlimeq  15476  sumeq1  15596  sumeq2w  15599  sumeq2ii  15600  sumeq2sdv  15610  zsum  15625  sumss2  15633  fsumsplitsnun  15662  isumclim3  15666  fsumcom2  15681  incexclem  15743  incexc2  15745  isumshft  15746  prodeq1f  15813  prodeq1  15814  prodeq2w  15817  prodeq2ii  15818  prodeq2sdv  15830  zprod  15844  fprodm1s  15877  fprodp1s  15878  fprodcom2  15891  fprodsplitf  15895  iprodclim3  15907  ef0lem  15985  ruclem7  16145  sadcp1  16366  smupp1  16391  smueqlem  16401  algrp1  16485  dfphi2  16685  prmdiveq  16697  pceulem  16757  vdwlem6  16898  cshwsiun  17011  sloteq  17094  setsid  17118  elbasfv  17126  elbasov  17127  imastset  17426  imasvscaval  17442  isoval  17672  funcoppc  17782  fulloppc  17831  fuccofval  17869  natpropd  17886  catccofval  18011  xpchomfval  18085  xpccofval  18088  lubfval  18254  glbfval  18267  chneq1  18518  chneq2  18519  grpidpropd  18570  gsumpropd2lem  18587  frmdplusg  18762  efmndplusg  18788  grpinvpropd  18928  grpsubpropd  18958  grpsubpropd2  18959  mulgpropd  19029  ecqusaddd  19104  oppgmnd  19266  sylow1lem2  19511  sylow3lem1  19539  prds1  20241  pwsmgp  20245  opprrng  20263  rngidpropd  20333  dvdsrpropd  20334  unitpropd  20335  invrpropd  20336  rhm1  20406  rhmopp  20424  rhmsubclem2  20601  lmhmpropd  21007  lidlrsppropd  21181  rngqiprnglinlem2  21229  lpival  21261  pzriprnglem11  21428  zrhpropd  21451  znle  21473  frlmplusgval  21701  frlmvscafval  21703  ressascl  21833  asclpropd  21834  aspval2  21835  psrbas  21870  psrplusg  21873  psrmulr  21879  psrvscafval  21885  resspsrbas  21911  ressmplbas2  21962  opsrle  21982  opsrbaslem  21984  vr1val  22104  ressply1add  22142  ressply1mul  22143  ressply1vsca  22144  psrplusgpropd  22148  mplbaspropd  22149  psropprmul  22150  ply1baspropd  22155  ply1plusgpropd  22156  ply1sca2  22166  ply1ascl0  22167  ply1ascl1  22168  subrgvr1  22175  coe1mul2lem2  22182  ply1coe1eq  22215  evls1addd  22286  evls1muld  22287  evls1vsca  22288  rhmply1vr1  22302  rhmply1vsca  22303  mamudi  22318  mamudir  22319  matrcl  22327  oftpos  22367  mattpos1  22371  mdetfval  22501  mdetrlin  22517  mdetrsca  22518  mdetrsca2  22519  mdetrlin2  22522  mdetunilem5  22531  madufval  22552  madugsum  22558  idmatidpmat  22652  cpmidpmat  22788  cncmp  23307  2ndcsep  23374  llyeq  23385  nllyeq  23386  xkouni  23514  hmphindis  23712  xkocnv  23729  ptcmplem2  23968  snclseqg  24031  prdstmdd  24039  ustexsym  24131  ucnextcn  24218  metreslem  24277  comet  24428  nrmmetd  24489  nmpropd  24509  isngp3  24513  ngpds  24519  subgnm  24548  tngnm  24566  idnghm  24658  cnmetdval  24685  cnmpopc  24849  htpyco2  24905  phtpyco2  24916  clsocv  25177  rrxprds  25316  rrxnm  25318  rrxplusgvscavalb  25322  ovolunlem1a  25424  voliunlem3  25480  ioombl1lem4  25489  uniioombllem4  25514  itg11  25619  itgeq1f  25699  itgeq1fOLD  25700  itgeq1  25701  itgeq2  25706  iblss2  25734  itgss  25740  itgeqa  25742  itgfsum  25755  itgsplit  25764  ditgeq1  25776  ditgeq2  25777  ditgeq3  25778  dvcmulf  25875  dvmptfsum  25906  dvcnvrelem2  25950  mdegfval  25994  mdegpropd  26016  deg1propd  26018  plyeq0  26143  coe11  26185  dgrlt  26199  dgradd2  26201  dgrmulc  26204  dvply1  26218  fta1lem  26242  pserulm  26358  rlimcnp2  26903  jensenlem1  26924  basellem5  27022  dchrbas  27173  dchrrcl  27178  dchrplusg  27185  dchrfi  27193  lgsdi  27272  lgseisenlem2  27314  lgsquadlem3  27320  dchrmusumlema  27431  rpvmasum2  27450  dchrisum0lema  27452  pntlemg  27536  nosupbnd2lem1  27654  lruneq  27852  addsval  27905  mulsval  28048  seqseq123d  28216  colperpexlem2  28709  axlowdimlem13  28932  uhgrvtxedgiedgb  29114  nb3grprlem1  29358  crctcshlem2  29796  wpthswwlks2on  29942  clwlknf1oclwwlkn  30064  frgrncvvdeq  30289  avril1  30443  0vfval  30586  imsval  30665  imsdval  30666  bcseqi  31100  normpythi  31122  cm0  31589  fh1  31598  pjcji  31664  opsqrlem5  32124  pjsdi2i  32137  pjclem3  32177  pjci  32180  golem1  32251  iuneq12daf  32536  iunrdx  32543  ofresid  32624  cnvprop  32677  coprprop  32680  f1od2  32702  dp2eq1  32853  dp2eq2  32854  fzto1st1  33071  gsumvsca1  33195  gsumvsca2  33196  urpropd  33199  resv1r  33304  nsgqusf1olem2  33379  oppr2idl  33451  opprqus0g  33455  ressply1evls1  33528  lindsunlem  33637  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  fldsdrgfldext2  33675  fldextrspunlem1  33688  fldextrspunfld  33689  algextdeglem4  33733  crefeq  33858  rspectopn  33880  xrge0mulc1cn  33954  qqhval2  33995  esumeq12dvaf  34044  esumeq2  34049  esumf1o  34063  esumfzf  34082  esumss  34085  esumpfinvalf  34089  ofceq  34110  carsgclctunlem1  34330  itgeq12dv  34339  ccatmulgnn0dir  34555  breprexpnat  34647  bnj956  34788  bnj1385  34844  bnj96  34877  bnj548  34909  bnj553  34910  bnj554  34911  bnj602  34927  bnj18eq1  34939  bnj1234  35025  bnj1296  35033  bnj1318  35037  bnj1442  35061  bnj1450  35062  cvmliftlem5  35333  cvmliftlem10  35338  cvmlift2lem9  35355  cvmliftphtlem  35361  satfdm  35413  mthmpps  35626  rdgprc  35836  dfrdg2  35837  wsuceq123  35856  wlimeq12  35861  altopthsn  36005  altxpeq1  36017  altxpeq2  36018  ixpeq12dv  36260  prodeq12sdv  36262  itgeq12sdv  36263  ditgeq123dv  36265  cbvcsbdavw  36303  cbvcsbdavw2  36304  cbvrabdavw  36305  cbviundavw  36306  cbviindavw  36307  cbvopab1davw  36308  cbvopab2davw  36309  cbvopabdavw  36310  cbvmptdavw  36311  cbviotadavw  36313  cbvriotadavw  36314  cbvoprab1davw  36315  cbvoprab2davw  36316  cbvoprab3davw  36317  cbvoprab123davw  36318  cbvoprab12davw  36319  cbvoprab23davw  36320  cbvoprab13davw  36321  cbvixpdavw  36322  cbvsumdavw  36323  cbvproddavw  36324  cbvitgdavw  36325  cbvditgdavw  36326  cbvrabdavw2  36329  cbviundavw2  36330  cbviindavw2  36331  cbvmptdavw2  36332  cbvriotadavw2  36334  cbvmpodavw2  36335  cbvmpo1davw2  36336  cbvmpo2davw2  36337  cbvixpdavw2  36338  cbvsumdavw2  36339  cbvproddavw2  36340  cbvitgdavw2  36341  cbvditgdavw2  36342  ee7.2aOLD  36505  bj-sngleq  37011  bj-tageq  37020  bj-projeq  37036  bj-projval  37040  bj-1upleq  37043  bj-pr1eq  37046  bj-pr2eq  37060  bj-evaleq  37116  bj-imafv  37295  csbrecsg  37372  csbrdgg  37373  csboprabg  37374  csbmpo123  37375  finxpeq1  37430  finxpeq2  37431  csbfinxpg  37432  finxpreclem4  37438  cureq  37635  unceq  37636  uncov  37640  unccur  37642  finixpnum  37644  ptrest  37658  poimirlem3  37662  poimirlem9  37668  poimirlem15  37674  poimirlem16  37675  poimirlem26  37685  poimirlem27  37686  mbfposadd  37706  cnambfre  37707  iblabsnclem  37722  ftc1anclem1  37732  heiborlem4  37853  heiborlem6  37855  mpobi123f  38201  iineq12f  38203  mptbi12f  38205  eccnvepres  38317  xrneq1  38419  xrneq2  38422  cosseq  38527  redundss3  38723  riotaclbgBAD  39052  toycom  39071  ldualvbase  39224  ldualfvadd  39226  ldualsca  39230  ldualsbase  39231  ldualsaddN  39232  ldualfvs  39234  ldual0  39245  ldual1  39246  ldualneg  39247  cdleme19f  40406  cdleme20m  40421  cdleme21k  40436  cdleme27b  40466  cdleme31so  40477  cdleme31sn  40478  cdleme31se  40480  cdleme31se2  40481  cdleme31sc  40482  cdleme31sde  40483  cdleme31fv  40488  cdleme40v  40567  cdleme43dN  40590  cdlemeg46ngfr  40616  ltrnco4  40837  tgrpbase  40844  tgrpopr  40845  erngbase  40899  erngfplus  40900  erngfmul  40903  erngbase-rN  40907  erngfplus-rN  40908  erngfmul-rN  40911  dvasca  41104  dvavbase  41111  dvafvadd  41112  dvafvsca  41114  tendocnv  41119  dvhsca  41180  dvhfplusr  41182  dvhvbase  41185  dvhfvadd  41189  dvhfvsca  41198  lcdvadd  41695  lcdsbase  41698  lcdsadd  41699  lcdvs  41701  lcd0  41706  lcd1  41707  lcdneg  41708  fsuppind  42682  imaiinfv  42785  mapfzcons1  42809  rexrabdioph  42886  dnnumch1  43136  dnwech  43140  aomclem6  43151  pwssplit4  43181  pwfi2f1o  43188  mendplusgfval  43273  mendvscafval  43278  harval3  43630  dssmapntrcls  44220  scotteqd  44329  colleq12d  44345  uzmptshftfval  44438  dropab1  44538  dropab2  44539  iineq12dv  45202  rabbida2  45228  rabbida3  45231  itgsinexplem1  46051  wallispi2lem2  46169  fourierdlem36  46240  etransclem4  46335  fcoreslem1  47162  afveq12d  47232  aoveq123d  47277  aovfundmoveq  47280  aovnuoveq  47290  aovvoveq  47291  aovovn0oveq  47293  afv2eq12d  47314  fsumsplitsndif  47472  rngccofvalALTV  48369  rhmsubcALTVlem2  48381  ringccofvalALTV  48403  itscnhlinecirc02plem2  48883  oppfrcl3  49230  oppf1st2nd  49231  uppropd  49281  natoppf  49329  catcrcl  49495  lmdpropd  49757  cmdpropd  49758  lmddu  49767  cmddu  49768  setrecseq  49785  aacllem  49901