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 2791	. 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  rabbidva2  3412  rabeqf  3416  rabeqiOLD  3418  csbeq1  3836  csbeq2  3838  csbeq2d  3839  difeq1  4051  difeq2  4052  uneq2  4092  ineq1  4140  ineq2  4141  symdifeq1  4179  symdifeq2  4180  dfrab3ss  4247  csbprc  4341  csbnestgfw  4354  csbnestgf  4359  disjssun  4402  ifeq1  4464  ifeq2  4465  pweqALT  4551  sneq  4572  csbsng  4645  csbprg  4646  preq1  4670  preq2  4671  tpeq1  4679  tpeq2  4680  tpeq3  4681  prprc1  4702  tpprceq3  4738  opeq1  4805  opeq2  4806  oteq1  4814  oteq2  4815  oteq3  4816  csbopg  4823  unieqOLD  4852  uniprg  4857  csbuni  4871  inteq  4883  iineq1  4942  iineq2  4945  iuneq12df  4951  dfiin2g  4963  iinrab  4999  iinin1  5009  iinxprg  5019  iununi  5029  opabbid  5140  opabbidv  5141  mpteq12da  5160  mpteq12dfOLD  5162  mpteq12f  5163  mpteq12dva  5164  csbmpt12  5471  xpeq1  5604  xpeq2  5611  rneq  5848  reseq1  5888  reseq2  5889  resima2  5929  resindm  5943  resmpt  5948  resmptf  5950  imaeq1  5967  imaeq2  5968  mptcnv  6048  xpdisj1  6069  xpdisj2  6070  resdisj  6077  dmpropg  6123  rnpropg  6130  cores  6157  cores2  6167  xpco  6196  predeq123  6207  csbpredg  6212  sspred  6215  predres  6246  suceq  6335  sucprc  6345  iotaeq  6408  iotabi  6409  fntpg  6501  imain  6526  f1oprswap  6769  fveq1  6782  fveq2  6783  fvres  6802  csbfv12  6826  fnimapr  6861  fvco2  6874  xpprsng  7021  residpr  7024  fsnunfv  7068  fsnunres  7069  funiunfv  7130  f1ofvswap  7187  fliftf  7195  isoini2  7219  riotaeqdv  7242  riotabidv  7243  riotauni  7247  riotabidva  7261  snriota  7275  oveq  7290  oveq1  7291  oveq2  7292  oprabbid  7349  oprabbidv  7350  mpoeq123  7356  mpoeq123dva  7358  mpoeq3dva  7361  resmpo  7403  ovres  7447  f1ocnvd  7529  ofeqd  7544  ofreq  7546  fpar  7965  frecseq123  8107  csbfrecsg  8109  wrecseq123  8139  wrecseq123OLD  8140  csbwrecsg  8146  onovuni  8182  recseq  8214  tfr2a  8235  rdgeq1  8251  rdgeq2  8252  rdgsucmptf  8268  frsucmpt  8278  seqomeq12  8294  seqomsuc  8297  omopthi  8500  eceq1  8545  eceq2  8547  qseq1  8561  qseq2  8562  uniqs  8575  ecinxp  8590  qsinxp  8591  erovlem  8611  ecopovtrn  8618  ixpeq1  8705  unfi  8964  supeq1  9213  supeq2  9216  supeq3  9217  supeq123d  9218  infeq1  9244  infeq2  9247  infeq3  9248  infeq123d  9249  infiso  9276  oieq1  9280  oieq2  9281  ordtypelem1  9286  inf3lemc  9393  wemapwe  9464  ttrcleq  9476  r1sucg  9536  r1limg  9538  rankprb  9618  karden  9662  djueq12  9671  cardiun  9749  acneq  9808  alephlim  9832  alephsuc  9833  alephfplem2  9870  infpssrlem2  10069  fin23lem34  10111  fin23lem35  10112  zorn2lem1  10261  zorn2lem7  10267  fpwwe2lem5  10400  fpwwe2lem12  10407  addpiord  10649  mulpiord  10650  addpqnq  10703  mulpqnq  10706  addassnq  10723  mulassnq  10724  distrnq  10726  lterpq  10735  ltexnq  10740  ltsrpr  10842  00sr  10864  recexsrlem  10868  mulgt0sr  10870  addcnsrec  10908  mulcnsrec  10909  negeq  11222  csbnegg  11227  negsubdi  11286  mulneg1  11420  negfi  11933  deceq1  12451  deceq2  12452  xnegeq  12950  fseq1p1m1  13339  om2uzrdg  13685  uzrdgsuci  13689  seqeq1  13733  seqeq2  13734  seqeq3  13735  seqfeq4  13781  seqof  13789  hashprg  14119  hashtpg  14208  csbwrdg  14256  s1eq  14314  cats1co  14578  s2eqd  14585  s3eqd  14586  s4eqd  14587  s5eqd  14588  s6eqd  14589  s7eqd  14590  s8eqd  14591  xpcogend  14694  shftval  14794  limsupgle  15195  lo1eq  15286  rlimeq  15287  sumeq1  15409  sumeq2w  15413  sumeq2ii  15414  zsum  15439  sumss2  15447  fsumsplitsnun  15476  isumclim3  15480  fsumcom2  15495  incexclem  15557  incexc2  15559  isumshft  15560  prodeq1f  15627  prodeq2w  15631  prodeq2ii  15632  zprod  15656  fprodm1s  15689  fprodp1s  15690  fprodcom2  15703  fprodsplitf  15707  iprodclim3  15719  ef0lem  15797  ruclem7  15954  sadcp1  16171  smupp1  16196  smueqlem  16206  algrp1  16288  dfphi2  16484  prmdiveq  16496  pceulem  16555  vdwlem6  16696  cshwsiun  16810  sloteq  16893  setsid  16918  elbasfv  16927  elbasov  16928  imastset  17242  imasvscaval  17258  isoval  17486  funcoppc  17599  fulloppc  17647  fuccofval  17685  natpropd  17703  catccofval  17828  xpchomfval  17905  xpccofval  17908  lubfval  18077  glbfval  18090  grpidpropd  18355  gsumpropd2lem  18372  frmdplusg  18502  efmndplusg  18528  grpinvpropd  18659  grpsubpropd  18689  grpsubpropd2  18690  mulgpropd  18754  oppgmnd  18970  sylow1lem2  19213  sylow3lem1  19241  prds1  19862  pwsmgp  19866  opprring  19882  rngidpropd  19946  dvdsrpropd  19947  unitpropd  19948  invrpropd  19949  rhm1  19983  lmhmpropd  20344  lidlrsppropd  20510  lpival  20525  zrhpropd  20725  znle  20749  frlmplusgval  20980  frlmvscafval  20982  ressascl  21109  asclpropd  21110  aspval2  21111  psrbas  21156  psrplusg  21159  psrmulr  21162  psrvscafval  21168  resspsrbas  21193  ressmplbas2  21237  opsrle  21257  opsrbaslem  21259  opsrbaslemOLD  21260  vr1val  21372  ressply1add  21410  ressply1mul  21411  ressply1vsca  21412  psrplusgpropd  21416  mplbaspropd  21417  psropprmul  21418  ply1baspropd  21423  ply1plusgpropd  21424  ply1sca2  21434  subrgvr1  21441  coe1mul2lem2  21448  ply1coe1eq  21478  mamudi  21559  mamudir  21560  matrcl  21568  oftpos  21610  mattpos1  21614  mdetfval  21744  mdetrlin  21760  mdetrsca  21761  mdetrsca2  21762  mdetrlin2  21765  mdetunilem5  21774  madufval  21795  madugsum  21801  idmatidpmat  21895  cpmidpmat  22031  cncmp  22552  2ndcsep  22619  llyeq  22630  nllyeq  22631  xkouni  22759  hmphindis  22957  xkocnv  22974  ptcmplem2  23213  snclseqg  23276  prdstmdd  23284  ustexsym  23376  ucnextcn  23465  metreslem  23524  comet  23678  nrmmetd  23739  nmpropd  23759  isngp3  23763  ngpds  23769  subgnm  23798  tngnm  23824  idnghm  23916  cnmetdval  23943  cnmpopc  24100  htpyco2  24151  phtpyco2  24162  clsocv  24423  rrxprds  24562  rrxnm  24564  rrxplusgvscavalb  24568  ovolunlem1a  24669  voliunlem3  24725  ioombl1lem4  24734  uniioombllem4  24759  itg11  24864  itgeq1f  24945  itgeq2  24951  iblss2  24979  itgss  24985  itgeqa  24987  itgfsum  25000  itgsplit  25009  ditgeq1  25021  ditgeq2  25022  ditgeq3  25023  dvcmulf  25118  dvmptfsum  25148  dvcnvrelem2  25191  mdegfval  25236  mdegpropd  25258  deg1propd  25260  plyeq0  25381  coe11  25423  dgrlt  25436  dgradd2  25438  dgrmulc  25441  dvply1  25453  fta1lem  25476  pserulm  25590  rlimcnp2  26125  jensenlem1  26145  basellem5  26243  dchrbas  26392  dchrrcl  26397  dchrplusg  26404  dchrfi  26412  lgsdi  26491  lgseisenlem2  26533  lgsquadlem3  26539  dchrmusumlema  26650  rpvmasum2  26669  dchrisum0lema  26671  pntlemg  26755  colperpexlem2  27101  axlowdimlem13  27331  uhgrvtxedgiedgb  27515  nb3grprlem1  27756  crctcshlem2  28192  wpthswwlks2on  28335  clwlknf1oclwwlkn  28457  frgrncvvdeq  28682  avril1  28836  0vfval  28977  imsval  29056  imsdval  29057  bcseqi  29491  normpythi  29513  cm0  29980  fh1  29989  pjcji  30055  opsqrlem5  30515  pjsdi2i  30528  pjclem3  30568  pjci  30571  golem1  30642  iuneq12daf  30905  iunrdx  30912  ofresid  30988  fnimatp  31023  cnvprop  31038  coprprop  31041  f1od2  31065  dp2eq1  31156  dp2eq2  31157  fzto1st1  31378  gsumvsca1  31488  gsumvsca2  31489  rhmopp  31527  resv1r  31550  nsgqusf1olem2  31608  lindsunlem  31714  fedgmullem1  31719  fedgmullem2  31720  fedgmul  31721  crefeq  31804  rspectopn  31826  xrge0mulc1cn  31900  qqhval2  31941  esumeq12dvaf  32008  esumeq2  32013  esumf1o  32027  esumfzf  32046  esumss  32049  esumpfinvalf  32053  ofceq  32074  carsgclctunlem1  32293  itgeq12dv  32302  ccatmulgnn0dir  32530  breprexpnat  32623  bnj956  32765  bnj1385  32821  bnj96  32854  bnj548  32886  bnj553  32887  bnj554  32888  bnj602  32904  bnj18eq1  32916  bnj1234  33002  bnj1296  33010  bnj1318  33014  bnj1442  33038  bnj1450  33039  cvmliftlem5  33260  cvmliftlem10  33265  cvmlift2lem9  33282  cvmliftphtlem  33288  satfdm  33340  mthmpps  33553  eqfunressuc  33745  rdgprc  33779  dfrdg2  33780  wsuceq123  33817  wlimeq12  33822  nosupbnd2lem1  33927  lruneq  34095  addsval  34135  altopthsn  34272  altxpeq1  34284  altxpeq2  34285  ee7.2aOLD  34659  bj-rabbida2  35115  bj-sngleq  35166  bj-tageq  35175  bj-projeq  35191  bj-projval  35195  bj-1upleq  35198  bj-pr1eq  35201  bj-pr2eq  35215  bj-evaleq  35252  bj-imafv  35431  csbrecsg  35508  csbrdgg  35509  csboprabg  35510  csbmpo123  35511  finxpeq1  35566  finxpeq2  35567  csbfinxpg  35568  finxpreclem4  35574  cureq  35762  unceq  35763  uncov  35767  unccur  35769  finixpnum  35771  ptrest  35785  poimirlem3  35789  poimirlem9  35795  poimirlem15  35801  poimirlem16  35802  poimirlem26  35812  poimirlem27  35813  mbfposadd  35833  cnambfre  35834  iblabsnclem  35849  ftc1anclem1  35859  heiborlem4  35981  heiborlem6  35983  mpobi123f  36329  iineq12f  36331  mptbi12f  36333  eccnvepres  36423  uniqsALTV  36471  xrneq1  36514  xrneq2  36517  cosseq  36556  redundss3  36748  riotaclbgBAD  36975  toycom  36994  ldualvbase  37147  ldualfvadd  37149  ldualsca  37153  ldualsbase  37154  ldualsaddN  37155  ldualfvs  37157  ldual0  37168  ldual1  37169  ldualneg  37170  cdleme19f  38329  cdleme20m  38344  cdleme21k  38359  cdleme27b  38389  cdleme31so  38400  cdleme31sn  38401  cdleme31se  38403  cdleme31se2  38404  cdleme31sc  38405  cdleme31sde  38406  cdleme31fv  38411  cdleme40v  38490  cdleme43dN  38513  cdlemeg46ngfr  38539  ltrnco4  38760  tgrpbase  38767  tgrpopr  38768  erngbase  38822  erngfplus  38823  erngfmul  38826  erngbase-rN  38830  erngfplus-rN  38831  erngfmul-rN  38834  dvasca  39027  dvavbase  39034  dvafvadd  39035  dvafvsca  39037  tendocnv  39042  dvhsca  39103  dvhfplusr  39105  dvhvbase  39108  dvhfvadd  39112  dvhfvsca  39121  lcdvadd  39618  lcdsbase  39621  lcdsadd  39622  lcdvs  39624  lcd0  39629  lcd1  39630  lcdneg  39631  mplascl0  40277  fsuppind  40286  imaiinfv  40522  mapfzcons1  40546  rexrabdioph  40623  dnnumch1  40876  dnwech  40880  aomclem6  40891  pwssplit4  40921  pwfi2f1o  40928  mendplusgfval  41017  mendvscafval  41022  harval3  41152  dssmapntrcls  41745  scotteqd  41862  colleq12d  41878  uzmptshftfval  41971  dropab1  42072  dropab2  42073  rabbida2  42688  rabbida3  42691  itgsinexplem1  43502  wallispi2lem2  43620  fourierdlem36  43691  etransclem4  43786  fcoreslem1  44568  afveq12d  44636  aoveq123d  44681  aovfundmoveq  44684  aovnuoveq  44694  aovvoveq  44695  aovovn0oveq  44697  afv2eq12d  44718  fsumsplitsndif  44836  rngccofvalALTV  45556  ringccofvalALTV  45619  rhmsubclem2  45656  rhmsubcALTVlem2  45674  itscnhlinecirc02plem2  46140  setrecseq  46402  aacllem  46516