Theorem 3eqtr4g 2804

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  rabbidva2  3400  rabeqf  3405  rabeqiOLD  3407  csbeq1  3831  csbeq2  3833  csbeq2d  3834  difeq1  4046  difeq2  4047  uneq2  4087  ineq1  4136  ineq2  4137  symdifeq1  4175  symdifeq2  4176  dfrab3ss  4243  csbprc  4337  csbnestgfw  4350  csbnestgf  4355  disjssun  4398  ifeq1  4460  ifeq2  4461  pweqALT  4547  sneq  4568  csbsng  4641  csbprg  4642  preq1  4666  preq2  4667  tpeq1  4675  tpeq2  4676  tpeq3  4677  prprc1  4698  tpprceq3  4734  opeq1  4801  opeq2  4802  oteq1  4810  oteq2  4811  oteq3  4812  csbopg  4819  unieqOLD  4848  uniprg  4853  csbuni  4867  inteq  4879  iineq1  4938  iineq2  4941  iuneq12df  4947  dfiin2g  4958  iinrab  4994  iinin1  5004  iinxprg  5014  iununi  5024  opabbid  5135  opabbidv  5136  mpteq12da  5155  mpteq12dfOLD  5157  mpteq12f  5158  mpteq12dva  5159  csbmpt12  5463  xpeq1  5594  xpeq2  5601  rneq  5834  reseq1  5874  reseq2  5875  resima2  5915  resindm  5929  resmpt  5934  resmptf  5936  imaeq1  5953  imaeq2  5954  mptcnv  6032  xpdisj1  6053  xpdisj2  6054  resdisj  6061  dmpropg  6107  rnpropg  6114  cores  6142  cores2  6152  xpco  6181  predeq123  6192  csbpredg  6197  sspred  6200  suceq  6316  sucprc  6326  iotaeq  6389  iotabi  6390  fntpg  6478  imain  6503  f1oprswap  6743  fveq1  6755  fveq2  6756  fvres  6775  csbfv12  6799  fnimapr  6834  fvco2  6847  xpprsng  6994  residpr  6997  fsnunfv  7041  fsnunres  7042  funiunfv  7103  f1ofvswap  7158  fliftf  7166  isoini2  7190  riotaeqdv  7213  riotabidv  7214  riotauni  7218  riotabidva  7232  snriota  7246  oveq  7261  oveq1  7262  oveq2  7263  oprabbid  7318  oprabbidv  7319  mpoeq123  7325  mpoeq123dva  7327  mpoeq3dva  7330  resmpo  7372  ovres  7416  f1ocnvd  7498  ofeqd  7513  ofreq  7515  fpar  7927  frecseq123  8069  csbfrecsg  8071  wrecseq123  8101  wrecseq123OLD  8102  csbwrecsg  8108  onovuni  8144  recseq  8176  tfr2a  8197  rdgeq1  8213  rdgeq2  8214  rdgsucmptf  8230  frsucmpt  8239  seqomeq12  8255  seqomsuc  8258  omopthi  8451  eceq1  8494  eceq2  8496  qseq1  8510  qseq2  8511  uniqs  8524  ecinxp  8539  qsinxp  8540  erovlem  8560  ecopovtrn  8567  ixpeq1  8654  unfi  8917  supeq1  9134  supeq2  9137  supeq3  9138  supeq123d  9139  infeq1  9165  infeq2  9168  infeq3  9169  infeq123d  9170  infiso  9197  oieq1  9201  oieq2  9202  ordtypelem1  9207  inf3lemc  9314  wemapwe  9385  trpredeq1  9398  trpredeq2  9399  trpredeq3  9400  r1sucg  9458  r1limg  9460  rankprb  9540  karden  9584  djueq12  9593  cardiun  9671  acneq  9730  alephlim  9754  alephsuc  9755  alephfplem2  9792  infpssrlem2  9991  fin23lem34  10033  fin23lem35  10034  zorn2lem1  10183  zorn2lem7  10189  fpwwe2lem5  10322  fpwwe2lem12  10329  addpiord  10571  mulpiord  10572  addpqnq  10625  mulpqnq  10628  addassnq  10645  mulassnq  10646  distrnq  10648  lterpq  10657  ltexnq  10662  ltsrpr  10764  00sr  10786  recexsrlem  10790  mulgt0sr  10792  addcnsrec  10830  mulcnsrec  10831  negeq  11143  csbnegg  11148  negsubdi  11207  mulneg1  11341  negfi  11854  deceq1  12371  deceq2  12372  xnegeq  12870  fseq1p1m1  13259  om2uzrdg  13604  uzrdgsuci  13608  seqeq1  13652  seqeq2  13653  seqeq3  13654  seqfeq4  13700  seqof  13708  hashprg  14038  hashtpg  14127  csbwrdg  14175  s1eq  14233  cats1co  14497  s2eqd  14504  s3eqd  14505  s4eqd  14506  s5eqd  14507  s6eqd  14508  s7eqd  14509  s8eqd  14510  xpcogend  14613  shftval  14713  limsupgle  15114  lo1eq  15205  rlimeq  15206  sumeq1  15328  sumeq2w  15332  sumeq2ii  15333  zsum  15358  sumss2  15366  fsumsplitsnun  15395  isumclim3  15399  fsumcom2  15414  incexclem  15476  incexc2  15478  isumshft  15479  prodeq1f  15546  prodeq2w  15550  prodeq2ii  15551  zprod  15575  fprodm1s  15608  fprodp1s  15609  fprodcom2  15622  fprodsplitf  15626  iprodclim3  15638  ef0lem  15716  ruclem7  15873  sadcp1  16090  smupp1  16115  smueqlem  16125  algrp1  16207  dfphi2  16403  prmdiveq  16415  pceulem  16474  vdwlem6  16615  cshwsiun  16729  sloteq  16812  setsid  16837  elbasfv  16846  elbasov  16847  imastset  17150  imasvscaval  17166  isoval  17394  funcoppc  17506  fulloppc  17554  fuccofval  17592  natpropd  17610  catccofval  17735  xpchomfval  17812  xpccofval  17815  lubfval  17983  glbfval  17996  grpidpropd  18261  gsumpropd2lem  18278  frmdplusg  18408  efmndplusg  18434  grpinvpropd  18565  grpsubpropd  18595  grpsubpropd2  18596  mulgpropd  18660  oppgmnd  18876  sylow1lem2  19119  sylow3lem1  19147  prds1  19768  pwsmgp  19772  opprring  19788  rngidpropd  19852  dvdsrpropd  19853  unitpropd  19854  invrpropd  19855  rhm1  19889  lmhmpropd  20250  lidlrsppropd  20414  lpival  20429  zrhpropd  20628  znle  20652  frlmplusgval  20881  frlmvscafval  20883  ressascl  21010  asclpropd  21011  aspval2  21012  psrbas  21057  psrplusg  21060  psrmulr  21063  psrvscafval  21069  resspsrbas  21094  ressmplbas2  21138  opsrle  21158  opsrbaslem  21160  opsrbaslemOLD  21161  vr1val  21273  ressply1add  21311  ressply1mul  21312  ressply1vsca  21313  psrplusgpropd  21317  mplbaspropd  21318  psropprmul  21319  ply1baspropd  21324  ply1plusgpropd  21325  ply1sca2  21335  subrgvr1  21342  coe1mul2lem2  21349  ply1coe1eq  21379  mamudi  21460  mamudir  21461  matrcl  21469  oftpos  21509  mattpos1  21513  mdetfval  21643  mdetrlin  21659  mdetrsca  21660  mdetrsca2  21661  mdetrlin2  21664  mdetunilem5  21673  madufval  21694  madugsum  21700  idmatidpmat  21794  cpmidpmat  21930  cncmp  22451  2ndcsep  22518  llyeq  22529  nllyeq  22530  xkouni  22658  hmphindis  22856  xkocnv  22873  ptcmplem2  23112  snclseqg  23175  prdstmdd  23183  ustexsym  23275  ucnextcn  23364  metreslem  23423  comet  23575  nrmmetd  23636  nmpropd  23656  isngp3  23660  ngpds  23666  subgnm  23695  tngnm  23721  idnghm  23813  cnmetdval  23840  cnmpopc  23997  htpyco2  24048  phtpyco2  24059  clsocv  24319  rrxprds  24458  rrxnm  24460  rrxplusgvscavalb  24464  ovolunlem1a  24565  voliunlem3  24621  ioombl1lem4  24630  uniioombllem4  24655  itg11  24760  itgeq1f  24841  itgeq2  24847  iblss2  24875  itgss  24881  itgeqa  24883  itgfsum  24896  itgsplit  24905  ditgeq1  24917  ditgeq2  24918  ditgeq3  24919  dvcmulf  25014  dvmptfsum  25044  dvcnvrelem2  25087  mdegfval  25132  mdegpropd  25154  deg1propd  25156  plyeq0  25277  coe11  25319  dgrlt  25332  dgradd2  25334  dgrmulc  25337  dvply1  25349  fta1lem  25372  pserulm  25486  rlimcnp2  26021  jensenlem1  26041  basellem5  26139  dchrbas  26288  dchrrcl  26293  dchrplusg  26300  dchrfi  26308  lgsdi  26387  lgseisenlem2  26429  lgsquadlem3  26435  dchrmusumlema  26546  rpvmasum2  26565  dchrisum0lema  26567  pntlemg  26651  colperpexlem2  26996  axlowdimlem13  27225  uhgrvtxedgiedgb  27409  nb3grprlem1  27650  crctcshlem2  28084  wpthswwlks2on  28227  clwlknf1oclwwlkn  28349  frgrncvvdeq  28574  avril1  28728  0vfval  28869  imsval  28948  imsdval  28949  bcseqi  29383  normpythi  29405  cm0  29872  fh1  29881  pjcji  29947  opsqrlem5  30407  pjsdi2i  30420  pjclem3  30460  pjci  30463  golem1  30534  iuneq12daf  30797  iunrdx  30804  ofresid  30880  fnimatp  30916  cnvprop  30931  coprprop  30934  f1od2  30958  dp2eq1  31049  dp2eq2  31050  fzto1st1  31271  gsumvsca1  31381  gsumvsca2  31382  rhmopp  31420  resv1r  31443  nsgqusf1olem2  31501  lindsunlem  31607  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  crefeq  31697  rspectopn  31719  xrge0mulc1cn  31793  qqhval2  31832  esumeq12dvaf  31899  esumeq2  31904  esumf1o  31918  esumfzf  31937  esumss  31940  esumpfinvalf  31944  ofceq  31965  carsgclctunlem1  32184  itgeq12dv  32193  ccatmulgnn0dir  32421  breprexpnat  32514  bnj956  32656  bnj1385  32712  bnj96  32745  bnj548  32777  bnj553  32778  bnj554  32779  bnj602  32795  bnj18eq1  32807  bnj1234  32893  bnj1296  32901  bnj1318  32905  bnj1442  32929  bnj1450  32930  cvmliftlem5  33151  cvmliftlem10  33156  cvmlift2lem9  33173  cvmliftphtlem  33179  satfdm  33231  mthmpps  33444  eqfunressuc  33642  rdgprc  33676  dfrdg2  33677  ttrcleq  33695  wsuceq123  33735  wlimeq12  33740  nosupbnd2lem1  33845  lruneq  34013  addsval  34053  altopthsn  34190  altxpeq1  34202  altxpeq2  34203  ee7.2aOLD  34577  bj-rabbida2  35033  bj-sngleq  35084  bj-tageq  35093  bj-projeq  35109  bj-projval  35113  bj-1upleq  35116  bj-pr1eq  35119  bj-pr2eq  35133  bj-evaleq  35170  bj-imafv  35349  csbrecsg  35426  csbrdgg  35427  csboprabg  35428  csbmpo123  35429  finxpeq1  35484  finxpeq2  35485  csbfinxpg  35486  finxpreclem4  35492  cureq  35680  unceq  35681  uncov  35685  unccur  35687  finixpnum  35689  ptrest  35703  poimirlem3  35707  poimirlem9  35713  poimirlem15  35719  poimirlem16  35720  poimirlem26  35730  poimirlem27  35731  mbfposadd  35751  cnambfre  35752  iblabsnclem  35767  ftc1anclem1  35777  heiborlem4  35899  heiborlem6  35901  mpobi123f  36247  iineq12f  36249  mptbi12f  36251  eccnvepres  36342  uniqsALTV  36391  xrneq1  36434  xrneq2  36437  cosseq  36476  redundss3  36668  riotaclbgBAD  36895  toycom  36914  ldualvbase  37067  ldualfvadd  37069  ldualsca  37073  ldualsbase  37074  ldualsaddN  37075  ldualfvs  37077  ldual0  37088  ldual1  37089  ldualneg  37090  cdleme19f  38249  cdleme20m  38264  cdleme21k  38279  cdleme27b  38309  cdleme31so  38320  cdleme31sn  38321  cdleme31se  38323  cdleme31se2  38324  cdleme31sc  38325  cdleme31sde  38326  cdleme31fv  38331  cdleme40v  38410  cdleme43dN  38433  cdlemeg46ngfr  38459  ltrnco4  38680  tgrpbase  38687  tgrpopr  38688  erngbase  38742  erngfplus  38743  erngfmul  38746  erngbase-rN  38750  erngfplus-rN  38751  erngfmul-rN  38754  dvasca  38947  dvavbase  38954  dvafvadd  38955  dvafvsca  38957  tendocnv  38962  dvhsca  39023  dvhfplusr  39025  dvhvbase  39028  dvhfvadd  39032  dvhfvsca  39041  lcdvadd  39538  lcdsbase  39541  lcdsadd  39542  lcdvs  39544  lcd0  39549  lcd1  39550  lcdneg  39551  fsuppind  40202  imaiinfv  40431  mapfzcons1  40455  rexrabdioph  40532  dnnumch1  40785  dnwech  40789  aomclem6  40800  pwssplit4  40830  pwfi2f1o  40837  mendplusgfval  40926  mendvscafval  40931  harval3  41041  dssmapntrcls  41627  scotteqd  41744  colleq12d  41760  uzmptshftfval  41853  dropab1  41954  dropab2  41955  rabbida2  42570  rabbida3  42573  itgsinexplem1  43385  wallispi2lem2  43503  fourierdlem36  43574  etransclem4  43669  fcoreslem1  44444  afveq12d  44512  aoveq123d  44557  aovfundmoveq  44560  aovnuoveq  44570  aovvoveq  44571  aovovn0oveq  44573  afv2eq12d  44594  fsumsplitsndif  44713  rngccofvalALTV  45433  ringccofvalALTV  45496  rhmsubclem2  45533  rhmsubcALTVlem2  45551  itscnhlinecirc02plem2  46017  setrecseq  46277  aacllem  46391