Theorem 3eqtr4g 2789

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 2776	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2782	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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  rabbidva2  3404  rabbida4  3428  rabeqf  3437  csbeq1  3862  csbeq2  3864  csbeq2d  3865  csbeq2dv  3866  difeq1  4078  difeq2  4079  uneq2  4121  ineq1  4172  ineq2  4173  symdifeq1  4214  symdifeq2  4215  dfrab3ss  4282  csbprc  4368  csbnestgfw  4381  csbnestgf  4386  disjssun  4427  ifeq1  4488  ifeq2  4489  pweqALT  4574  sneq  4595  rabsneq  4604  csbsng  4668  csbprg  4669  preq1  4693  preq2  4694  tpeq1  4702  tpeq2  4703  tpeq3  4704  prprc1  4725  tpprceq3  4764  opeq1  4833  opeq2  4834  oteq1  4842  oteq2  4843  oteq3  4844  csbopg  4851  uniprg  4883  csbuni  4896  inteq  4909  iineq1  4969  iineq2  4972  iuneq12df  4978  iuneq12d  4981  dfiin2g  4991  iinrab  5028  iinin1  5038  iinxprg  5048  iununi  5058  opabbid  5167  opabbidv  5168  mpteq12da  5185  mpteq12f  5187  mpteq12dva  5188  csbmpt12  5512  xpeq1  5645  xpeq2  5652  rneq  5889  reseq1  5933  reseq2  5934  resima2  5976  resindm  5990  resmpt  5997  resmptf  5999  imaeq1  6015  imaeq2  6016  mptcnv  6100  xpdisj1  6122  xpdisj2  6123  resdisj  6130  dmpropg  6176  rnpropg  6183  cores  6210  cores2  6220  xpco  6250  predeq123  6263  csbpredg  6268  sspred  6271  predres  6300  suceqd  6387  sucprc  6398  iotaeq  6464  iotabi  6465  fntpg  6560  imain  6585  f1oprswap  6826  fveq1  6839  fveq2  6840  fvres  6859  csbfv12  6888  fnimapr  6926  fnimatpd  6927  fvco2  6940  xpprsng  7094  residpr  7097  fsnunfv  7143  fsnunres  7144  funiunfv  7204  f1ofvswap  7263  fliftf  7272  isoini2  7296  eqfunressuc  7318  riotaeqdv  7327  riotabidv  7328  riotauni  7332  riotabidva  7345  snriota  7359  oveq  7375  oveq1  7376  oveq2  7377  oprabbid  7434  oprabbidv  7435  mpoeq123  7441  mpoeq123dva  7443  mpoeq3dva  7446  resmpo  7489  ovres  7535  f1ocnvd  7620  ofeqd  7635  ofreq  7637  fpar  8072  frecseq123  8238  csbfrecsg  8240  wrecseq123  8269  csbwrecsg  8274  onovuni  8288  recseq  8319  tfr2a  8340  rdgeq1  8356  rdgeq2  8357  rdgsucmptf  8373  frsucmpt  8383  seqomeq12  8399  seqomsuc  8402  omopthi  8602  eceq1  8687  eceq2  8689  qseq1  8707  qseq2  8708  uniqs  8724  ecinxp  8742  qsinxp  8743  erovlem  8763  ecopovtrn  8770  ixpeq1  8858  unfi  9112  supeq1  9372  supeq2  9375  supeq3  9376  supeq123d  9377  infeq1  9404  infeq2  9407  infeq3  9408  infeq123d  9409  infiso  9437  oieq1  9441  oieq2  9442  ordtypelem1  9447  inf3lemc  9555  wemapwe  9626  ttrcleq  9638  r1sucg  9698  r1limg  9700  rankprb  9780  karden  9824  djueq12  9833  cardiun  9911  acneq  9972  alephlim  9996  alephsuc  9997  alephfplem2  10034  infpssrlem2  10233  fin23lem34  10275  fin23lem35  10276  zorn2lem1  10425  zorn2lem7  10431  fpwwe2lem5  10564  fpwwe2lem12  10571  addpiord  10813  mulpiord  10814  addpqnq  10867  mulpqnq  10870  addassnq  10887  mulassnq  10888  distrnq  10890  lterpq  10899  ltexnq  10904  ltsrpr  11006  00sr  11028  recexsrlem  11032  mulgt0sr  11034  addcnsrec  11072  mulcnsrec  11073  negeq  11389  csbnegg  11394  negsubdi  11454  mulneg1  11590  negfi  12108  deceq1  12630  deceq2  12631  xnegeq  13143  fseq1p1m1  13535  om2uzrdg  13897  uzrdgsuci  13901  seqeq1  13945  seqeq2  13946  seqeq3  13947  seqfeq4  13992  seqof  14000  hashprg  14336  hashtpg  14426  csbwrdg  14485  s1eq  14541  cats1co  14798  s2eqd  14805  s3eqd  14806  s4eqd  14807  s5eqd  14808  s6eqd  14809  s7eqd  14810  s8eqd  14811  xpcogend  14916  shftval  15016  limsupgle  15419  lo1eq  15510  rlimeq  15511  sumeq1  15631  sumeq2w  15634  sumeq2ii  15635  sumeq2sdv  15645  zsum  15660  sumss2  15668  fsumsplitsnun  15697  isumclim3  15701  fsumcom2  15716  incexclem  15778  incexc2  15780  isumshft  15781  prodeq1f  15848  prodeq1  15849  prodeq2w  15852  prodeq2ii  15853  prodeq2sdv  15865  zprod  15879  fprodm1s  15912  fprodp1s  15913  fprodcom2  15926  fprodsplitf  15930  iprodclim3  15942  ef0lem  16020  ruclem7  16180  sadcp1  16401  smupp1  16426  smueqlem  16436  algrp1  16520  dfphi2  16720  prmdiveq  16732  pceulem  16792  vdwlem6  16933  cshwsiun  17046  sloteq  17129  setsid  17153  elbasfv  17161  elbasov  17162  imastset  17461  imasvscaval  17477  isoval  17707  funcoppc  17817  fulloppc  17866  fuccofval  17904  natpropd  17921  catccofval  18046  xpchomfval  18120  xpccofval  18123  lubfval  18289  glbfval  18302  grpidpropd  18571  gsumpropd2lem  18588  frmdplusg  18763  efmndplusg  18789  grpinvpropd  18929  grpsubpropd  18959  grpsubpropd2  18960  mulgpropd  19030  ecqusaddd  19106  oppgmnd  19268  sylow1lem2  19513  sylow3lem1  19541  prds1  20243  pwsmgp  20247  opprrng  20265  rngidpropd  20335  dvdsrpropd  20336  unitpropd  20337  invrpropd  20338  rhm1  20409  rhmopp  20429  rhmsubclem2  20606  lmhmpropd  21012  lidlrsppropd  21186  rngqiprnglinlem2  21234  lpival  21266  pzriprnglem11  21433  zrhpropd  21456  znle  21478  frlmplusgval  21706  frlmvscafval  21708  ressascl  21838  asclpropd  21839  aspval2  21840  psrbas  21875  psrplusg  21878  psrmulr  21884  psrvscafval  21890  resspsrbas  21916  ressmplbas2  21967  opsrle  21987  opsrbaslem  21989  vr1val  22109  ressply1add  22147  ressply1mul  22148  ressply1vsca  22149  psrplusgpropd  22153  mplbaspropd  22154  psropprmul  22155  ply1baspropd  22160  ply1plusgpropd  22161  ply1sca2  22171  ply1ascl0  22172  ply1ascl1  22173  subrgvr1  22180  coe1mul2lem2  22187  ply1coe1eq  22220  evls1addd  22291  evls1muld  22292  evls1vsca  22293  rhmply1vr1  22307  rhmply1vsca  22308  mamudi  22323  mamudir  22324  matrcl  22332  oftpos  22372  mattpos1  22376  mdetfval  22506  mdetrlin  22522  mdetrsca  22523  mdetrsca2  22524  mdetrlin2  22527  mdetunilem5  22536  madufval  22557  madugsum  22563  idmatidpmat  22657  cpmidpmat  22793  cncmp  23312  2ndcsep  23379  llyeq  23390  nllyeq  23391  xkouni  23519  hmphindis  23717  xkocnv  23734  ptcmplem2  23973  snclseqg  24036  prdstmdd  24044  ustexsym  24136  ucnextcn  24224  metreslem  24283  comet  24434  nrmmetd  24495  nmpropd  24515  isngp3  24519  ngpds  24525  subgnm  24554  tngnm  24572  idnghm  24664  cnmetdval  24691  cnmpopc  24855  htpyco2  24911  phtpyco2  24922  clsocv  25183  rrxprds  25322  rrxnm  25324  rrxplusgvscavalb  25328  ovolunlem1a  25430  voliunlem3  25486  ioombl1lem4  25495  uniioombllem4  25520  itg11  25625  itgeq1f  25705  itgeq1fOLD  25706  itgeq1  25707  itgeq2  25712  iblss2  25740  itgss  25746  itgeqa  25748  itgfsum  25761  itgsplit  25770  ditgeq1  25782  ditgeq2  25783  ditgeq3  25784  dvcmulf  25881  dvmptfsum  25912  dvcnvrelem2  25956  mdegfval  26000  mdegpropd  26022  deg1propd  26024  plyeq0  26149  coe11  26191  dgrlt  26205  dgradd2  26207  dgrmulc  26210  dvply1  26224  fta1lem  26248  pserulm  26364  rlimcnp2  26909  jensenlem1  26930  basellem5  27028  dchrbas  27179  dchrrcl  27184  dchrplusg  27191  dchrfi  27199  lgsdi  27278  lgseisenlem2  27320  lgsquadlem3  27326  dchrmusumlema  27437  rpvmasum2  27456  dchrisum0lema  27458  pntlemg  27542  nosupbnd2lem1  27660  lruneq  27856  addsval  27909  mulsval  28052  seqseq123d  28220  colperpexlem2  28711  axlowdimlem13  28934  uhgrvtxedgiedgb  29116  nb3grprlem1  29360  crctcshlem2  29798  wpthswwlks2on  29941  clwlknf1oclwwlkn  30063  frgrncvvdeq  30288  avril1  30442  0vfval  30585  imsval  30664  imsdval  30665  bcseqi  31099  normpythi  31121  cm0  31588  fh1  31597  pjcji  31663  opsqrlem5  32123  pjsdi2i  32136  pjclem3  32176  pjci  32179  golem1  32250  iuneq12daf  32535  iunrdx  32542  ofresid  32616  cnvprop  32669  coprprop  32672  f1od2  32694  dp2eq1  32843  dp2eq2  32844  fzto1st1  33074  gsumvsca1  33195  gsumvsca2  33196  urpropd  33199  resv1r  33304  nsgqusf1olem2  33378  oppr2idl  33450  opprqus0g  33454  ressply1evls1  33527  lindsunlem  33613  fedgmullem1  33618  fedgmullem2  33619  fedgmul  33620  fldsdrgfldext2  33651  fldextrspunlem1  33663  fldextrspunfld  33664  algextdeglem4  33703  crefeq  33828  rspectopn  33850  xrge0mulc1cn  33924  qqhval2  33965  esumeq12dvaf  34014  esumeq2  34019  esumf1o  34033  esumfzf  34052  esumss  34055  esumpfinvalf  34059  ofceq  34080  carsgclctunlem1  34301  itgeq12dv  34310  ccatmulgnn0dir  34526  breprexpnat  34618  bnj956  34759  bnj1385  34815  bnj96  34848  bnj548  34880  bnj553  34881  bnj554  34882  bnj602  34898  bnj18eq1  34910  bnj1234  34996  bnj1296  35004  bnj1318  35008  bnj1442  35032  bnj1450  35033  cvmliftlem5  35269  cvmliftlem10  35274  cvmlift2lem9  35291  cvmliftphtlem  35297  satfdm  35349  mthmpps  35562  rdgprc  35775  dfrdg2  35776  wsuceq123  35795  wlimeq12  35800  altopthsn  35942  altxpeq1  35954  altxpeq2  35955  ixpeq12dv  36197  prodeq12sdv  36199  itgeq12sdv  36200  ditgeq123dv  36202  cbvcsbdavw  36240  cbvcsbdavw2  36241  cbvrabdavw  36242  cbviundavw  36243  cbviindavw  36244  cbvopab1davw  36245  cbvopab2davw  36246  cbvopabdavw  36247  cbvmptdavw  36248  cbviotadavw  36250  cbvriotadavw  36251  cbvoprab1davw  36252  cbvoprab2davw  36253  cbvoprab3davw  36254  cbvoprab123davw  36255  cbvoprab12davw  36256  cbvoprab23davw  36257  cbvoprab13davw  36258  cbvixpdavw  36259  cbvsumdavw  36260  cbvproddavw  36261  cbvitgdavw  36262  cbvditgdavw  36263  cbvrabdavw2  36266  cbviundavw2  36267  cbviindavw2  36268  cbvmptdavw2  36269  cbvriotadavw2  36271  cbvmpodavw2  36272  cbvmpo1davw2  36273  cbvmpo2davw2  36274  cbvixpdavw2  36275  cbvsumdavw2  36276  cbvproddavw2  36277  cbvitgdavw2  36278  cbvditgdavw2  36279  ee7.2aOLD  36442  bj-sngleq  36948  bj-tageq  36957  bj-projeq  36973  bj-projval  36977  bj-1upleq  36980  bj-pr1eq  36983  bj-pr2eq  36997  bj-evaleq  37053  bj-imafv  37232  csbrecsg  37309  csbrdgg  37310  csboprabg  37311  csbmpo123  37312  finxpeq1  37367  finxpeq2  37368  csbfinxpg  37369  finxpreclem4  37375  cureq  37583  unceq  37584  uncov  37588  unccur  37590  finixpnum  37592  ptrest  37606  poimirlem3  37610  poimirlem9  37616  poimirlem15  37622  poimirlem16  37623  poimirlem26  37633  poimirlem27  37634  mbfposadd  37654  cnambfre  37655  iblabsnclem  37670  ftc1anclem1  37680  heiborlem4  37801  heiborlem6  37803  mpobi123f  38149  iineq12f  38151  mptbi12f  38153  eccnvepres  38261  xrneq1  38356  xrneq2  38359  cosseq  38410  redundss3  38612  riotaclbgBAD  38940  toycom  38959  ldualvbase  39112  ldualfvadd  39114  ldualsca  39118  ldualsbase  39119  ldualsaddN  39120  ldualfvs  39122  ldual0  39133  ldual1  39134  ldualneg  39135  cdleme19f  40295  cdleme20m  40310  cdleme21k  40325  cdleme27b  40355  cdleme31so  40366  cdleme31sn  40367  cdleme31se  40369  cdleme31se2  40370  cdleme31sc  40371  cdleme31sde  40372  cdleme31fv  40377  cdleme40v  40456  cdleme43dN  40479  cdlemeg46ngfr  40505  ltrnco4  40726  tgrpbase  40733  tgrpopr  40734  erngbase  40788  erngfplus  40789  erngfmul  40792  erngbase-rN  40796  erngfplus-rN  40797  erngfmul-rN  40800  dvasca  40993  dvavbase  41000  dvafvadd  41001  dvafvsca  41003  tendocnv  41008  dvhsca  41069  dvhfplusr  41071  dvhvbase  41074  dvhfvadd  41078  dvhfvsca  41087  lcdvadd  41584  lcdsbase  41587  lcdsadd  41588  lcdvs  41590  lcd0  41595  lcd1  41596  lcdneg  41597  fsuppind  42571  imaiinfv  42674  mapfzcons1  42698  rexrabdioph  42775  dnnumch1  43026  dnwech  43030  aomclem6  43041  pwssplit4  43071  pwfi2f1o  43078  mendplusgfval  43163  mendvscafval  43168  harval3  43520  dssmapntrcls  44110  scotteqd  44219  colleq12d  44235  uzmptshftfval  44328  dropab1  44429  dropab2  44430  iineq12dv  45093  rabbida2  45119  rabbida3  45122  itgsinexplem1  45945  wallispi2lem2  46063  fourierdlem36  46134  etransclem4  46229  fcoreslem1  47057  afveq12d  47127  aoveq123d  47172  aovfundmoveq  47175  aovnuoveq  47185  aovvoveq  47186  aovovn0oveq  47188  afv2eq12d  47209  fsumsplitsndif  47367  rngccofvalALTV  48251  rhmsubcALTVlem2  48263  ringccofvalALTV  48285  itscnhlinecirc02plem2  48765  oppfrcl3  49112  oppf1st2nd  49113  uppropd  49163  natoppf  49211  catcrcl  49377  lmdpropd  49639  cmdpropd  49640  lmddu  49649  cmddu  49650  setrecseq  49667  aacllem  49783