Theorem 3eqtr4g 2858

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

Syntax hints:   → wi 4   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  rabbidva2  3423  rabeqf  3428  rabeqiOLD  3430  csbeq1  3831  csbeq2  3833  csbeq2d  3834  difeq1  4043  difeq2  4044  uneq2  4084  ineq1  4131  ineq2  4133  symdifeq1  4171  symdifeq2  4172  dfrab3ss  4233  csbprc  4313  csbnestgfw  4327  csbnestgf  4332  disjssun  4375  ifeq1  4429  ifeq2  4430  pweqALT  4514  sneq  4535  csbsng  4604  csbprg  4605  preq1  4629  preq2  4630  tpeq1  4638  tpeq2  4639  tpeq3  4640  prprc1  4661  tpprceq3  4697  opeq1  4763  opeq1OLD  4764  opeq2  4765  opeq2OLD  4766  oteq1  4774  oteq2  4775  oteq3  4776  csbopg  4783  unieqOLD  4812  csbuni  4829  inteq  4841  iineq1  4898  iineq2  4901  iuneq12df  4907  dfiin2g  4919  iinrab  4954  iinin1  4964  iinxprg  4974  iununi  4984  opabbid  5095  mpteq12df  5112  mpteq12f  5113  csbmpt12  5409  xpeq1  5533  xpeq2  5540  rneq  5770  reseq1  5812  reseq2  5813  resima2  5853  resindm  5867  resmpt  5872  resmptf  5874  imaeq1  5891  imaeq2  5892  mptcnv  5965  xpdisj1  5985  xpdisj2  5986  resdisj  5993  dmpropg  6039  rnpropg  6046  cores  6069  cores2  6079  xpco  6108  predeq123  6117  sspred  6124  suceq  6224  sucprc  6234  iotaeq  6295  iotabi  6296  fntpg  6384  imain  6409  f1oprswap  6633  fveq1  6644  fveq2  6645  fvres  6664  csbfv12  6688  fnimapr  6722  fvco2  6735  xpprsng  6879  residpr  6882  fsnunfv  6926  fsnunres  6927  funiunfv  6985  fliftf  7047  isoini2  7071  riotaeqdv  7094  riotabidv  7095  riotauni  7099  riotabidva  7112  snriota  7126  oveq  7141  oveq1  7142  oveq2  7143  oprabbid  7198  mpoeq123  7205  mpoeq123dva  7207  mpoeq3dva  7210  resmpo  7251  ovres  7294  f1ocnvd  7376  ofeq  7391  ofreq  7392  fpar  7794  wrecseq123  7931  onovuni  7962  recseq  7993  tfr2a  8014  rdgeq1  8030  rdgeq2  8031  rdgsucmptf  8047  frsucmpt  8056  seqomeq12  8073  seqomsuc  8076  omopthi  8267  eceq1  8310  eceq2  8312  qseq1  8326  qseq2  8327  uniqs  8340  ecinxp  8355  qsinxp  8356  erovlem  8376  ecopovtrn  8383  ixpeq1  8455  supeq1  8893  supeq2  8896  supeq3  8897  supeq123d  8898  infeq1  8924  infeq2  8927  infeq3  8928  infeq123d  8929  infiso  8956  oieq1  8960  oieq2  8961  ordtypelem1  8966  inf3lemc  9073  wemapwe  9144  r1sucg  9182  r1limg  9184  rankprb  9264  karden  9308  djueq12  9317  cardiun  9395  acneq  9454  alephlim  9478  alephsuc  9479  alephfplem2  9516  infpssrlem2  9715  fin23lem34  9757  fin23lem35  9758  zorn2lem1  9907  zorn2lem7  9913  fpwwe2lem6  10046  fpwwe2lem13  10053  addpiord  10295  mulpiord  10296  addpqnq  10349  mulpqnq  10352  addassnq  10369  mulassnq  10370  distrnq  10372  lterpq  10381  ltexnq  10386  ltsrpr  10488  00sr  10510  recexsrlem  10514  mulgt0sr  10516  addcnsrec  10554  mulcnsrec  10555  negeq  10867  csbnegg  10872  negsubdi  10931  mulneg1  11065  negfi  11577  deceq1  12091  deceq2  12092  xnegeq  12588  fseq1p1m1  12976  om2uzrdg  13319  uzrdgsuci  13323  seqeq1  13367  seqeq2  13368  seqeq3  13369  seqfeq4  13415  seqof  13423  hashprg  13752  hashtpg  13839  csbwrdg  13887  s1eq  13945  cats1co  14209  s2eqd  14216  s3eqd  14217  s4eqd  14218  s5eqd  14219  s6eqd  14220  s7eqd  14221  s8eqd  14222  xpcogend  14325  shftval  14425  limsupgle  14826  lo1eq  14917  rlimeq  14918  sumeq1  15037  sumeq2w  15041  sumeq2ii  15042  zsum  15067  sumss2  15075  fsumsplitsnun  15102  isumclim3  15106  fsumcom2  15121  incexclem  15183  incexc2  15185  isumshft  15186  prodeq1f  15254  prodeq2w  15258  prodeq2ii  15259  zprod  15283  fprodm1s  15316  fprodp1s  15317  fprodcom2  15330  fprodsplitf  15334  iprodclim3  15346  ef0lem  15424  ruclem7  15581  sadcp1  15794  smupp1  15819  smueqlem  15829  algrp1  15908  dfphi2  16101  prmdiveq  16113  pceulem  16172  vdwlem6  16312  cshwsiun  16425  sloteq  16480  setsid  16530  elbasfv  16536  elbasov  16537  imastset  16787  imasvscaval  16803  isoval  17027  funcoppc  17137  fulloppc  17184  fuccofval  17221  natpropd  17238  catccofval  17352  xpchomfval  17421  xpccofval  17424  lubfval  17580  glbfval  17593  grpidpropd  17864  gsumpropd2lem  17881  frmdplusg  18011  efmndplusg  18037  grpinvpropd  18166  grpsubpropd  18196  grpsubpropd2  18197  mulgpropd  18261  oppgmnd  18474  sylow1lem2  18716  sylow3lem1  18744  prds1  19360  pwsmgp  19364  opprring  19377  rngidpropd  19441  dvdsrpropd  19442  unitpropd  19443  invrpropd  19444  rhm1  19478  lmhmpropd  19838  lidlrsppropd  19996  lpival  20011  zrhpropd  20208  znle  20228  frlmplusgval  20453  frlmvscafval  20455  ressascl  20582  asclpropd  20583  aspval2  20584  psrbas  20616  psrplusg  20619  psrmulr  20622  psrvscafval  20628  resspsrbas  20653  ressmplbas2  20695  opsrle  20715  opsrbaslem  20717  vr1val  20821  ressply1add  20859  ressply1mul  20860  ressply1vsca  20861  psrplusgpropd  20865  mplbaspropd  20866  psropprmul  20867  ply1baspropd  20872  ply1plusgpropd  20873  ply1sca2  20883  subrgvr1  20890  coe1mul2lem2  20897  ply1coe1eq  20927  mamudi  21008  mamudir  21009  matrcl  21017  oftpos  21057  mattpos1  21061  mdetfval  21191  mdetrlin  21207  mdetrsca  21208  mdetrsca2  21209  mdetrlin2  21212  mdetunilem5  21221  madufval  21242  madugsum  21248  idmatidpmat  21342  cpmidpmat  21478  cncmp  21997  2ndcsep  22064  llyeq  22075  nllyeq  22076  xkouni  22204  hmphindis  22402  xkocnv  22419  ptcmplem2  22658  snclseqg  22721  prdstmdd  22729  ustexsym  22821  ucnextcn  22910  metreslem  22969  comet  23120  nrmmetd  23181  nmpropd  23200  isngp3  23204  ngpds  23210  subgnm  23239  tngnm  23257  idnghm  23349  cnmetdval  23376  cnmpopc  23533  htpyco2  23584  phtpyco2  23595  clsocv  23854  rrxprds  23993  rrxnm  23995  rrxplusgvscavalb  23999  ovolunlem1a  24100  voliunlem3  24156  ioombl1lem4  24165  uniioombllem4  24190  itg11  24295  itgeq1f  24375  itgeq2  24381  iblss2  24409  itgss  24415  itgeqa  24417  itgfsum  24430  itgsplit  24439  ditgeq1  24451  ditgeq2  24452  ditgeq3  24453  dvcmulf  24548  dvmptfsum  24578  dvcnvrelem2  24621  mdegfval  24663  mdegpropd  24685  deg1propd  24687  plyeq0  24808  coe11  24850  dgrlt  24863  dgradd2  24865  dgrmulc  24868  dvply1  24880  fta1lem  24903  pserulm  25017  rlimcnp2  25552  jensenlem1  25572  basellem5  25670  dchrbas  25819  dchrrcl  25824  dchrplusg  25831  dchrfi  25839  lgsdi  25918  lgseisenlem2  25960  lgsquadlem3  25966  dchrmusumlema  26077  rpvmasum2  26096  dchrisum0lema  26098  pntlemg  26182  colperpexlem2  26525  axlowdimlem13  26748  uhgrvtxedgiedgb  26929  nb3grprlem1  27170  crctcshlem2  27604  wpthswwlks2on  27747  clwlknf1oclwwlkn  27869  frgrncvvdeq  28094  avril1  28248  0vfval  28389  imsval  28468  imsdval  28469  bcseqi  28903  normpythi  28925  cm0  29392  fh1  29401  pjcji  29467  opsqrlem5  29927  pjsdi2i  29940  pjclem3  29980  pjci  29983  golem1  30054  iuneq12daf  30320  iunrdx  30327  ofresid  30403  fnimatp  30440  cnvprop  30456  coprprop  30459  f1od2  30483  dp2eq1  30575  dp2eq2  30576  fzto1st1  30794  gsumvsca1  30904  gsumvsca2  30905  rhmopp  30943  resv1r  30961  lindsunlem  31108  fedgmullem1  31113  fedgmullem2  31114  fedgmul  31115  crefeq  31198  rspectopn  31220  xrge0mulc1cn  31294  qqhval2  31333  esumeq12dvaf  31400  esumeq2  31405  esumf1o  31419  esumfzf  31438  esumss  31441  esumpfinvalf  31445  ofceq  31466  carsgclctunlem1  31685  itgeq12dv  31694  ccatmulgnn0dir  31922  breprexpnat  32015  bnj956  32158  bnj1385  32214  bnj96  32247  bnj548  32279  bnj553  32280  bnj554  32281  bnj602  32297  bnj18eq1  32309  bnj1234  32395  bnj1296  32403  bnj1318  32407  bnj1442  32431  bnj1450  32432  cvmliftlem5  32649  cvmliftlem10  32654  cvmlift2lem9  32671  cvmliftphtlem  32677  satfdm  32729  mthmpps  32942  eqfunressuc  33118  rdgprc  33152  dfrdg2  33153  trpredeq1  33172  trpredeq2  33173  trpredeq3  33174  wsuceq123  33214  wlimeq12  33219  frecseq123  33232  nosupbnd2lem1  33328  altopthsn  33535  altxpeq1  33547  altxpeq2  33548  ee7.2aOLD  33922  bj-rabbida2  34361  bj-sngleq  34403  bj-tageq  34412  bj-projeq  34428  bj-projval  34432  bj-1upleq  34435  bj-pr1eq  34438  bj-pr2eq  34452  bj-evaleq  34487  bj-imafv  34666  bj-isrvec  34708  csbpredg  34743  csbwrecsg  34744  csbrecsg  34745  csbrdgg  34746  csboprabg  34747  csbmpo123  34748  finxpeq1  34803  finxpeq2  34804  csbfinxpg  34805  finxpreclem4  34811  cureq  35033  unceq  35034  uncov  35038  unccur  35040  finixpnum  35042  ptrest  35056  poimirlem3  35060  poimirlem9  35066  poimirlem15  35072  poimirlem16  35073  poimirlem26  35083  poimirlem27  35084  mbfposadd  35104  cnambfre  35105  iblabsnclem  35120  ftc1anclem1  35130  heiborlem4  35252  heiborlem6  35254  mpobi123f  35600  iineq12f  35602  mptbi12f  35604  eccnvepres  35697  uniqsALTV  35746  xrneq1  35789  xrneq2  35792  cosseq  35831  redundss3  36023  riotaclbgBAD  36250  toycom  36269  ldualvbase  36422  ldualfvadd  36424  ldualsca  36428  ldualsbase  36429  ldualsaddN  36430  ldualfvs  36432  ldual0  36443  ldual1  36444  ldualneg  36445  cdleme19f  37604  cdleme20m  37619  cdleme21k  37634  cdleme27b  37664  cdleme31so  37675  cdleme31sn  37676  cdleme31se  37678  cdleme31se2  37679  cdleme31sc  37680  cdleme31sde  37681  cdleme31fv  37686  cdleme40v  37765  cdleme43dN  37788  cdlemeg46ngfr  37814  ltrnco4  38035  tgrpbase  38042  tgrpopr  38043  erngbase  38097  erngfplus  38098  erngfmul  38101  erngbase-rN  38105  erngfplus-rN  38106  erngfmul-rN  38109  dvasca  38302  dvavbase  38309  dvafvadd  38310  dvafvsca  38312  tendocnv  38317  dvhsca  38378  dvhfplusr  38380  dvhvbase  38383  dvhfvadd  38387  dvhfvsca  38396  lcdvadd  38893  lcdsbase  38896  lcdsadd  38897  lcdvs  38899  lcd0  38904  lcd1  38905  lcdneg  38906  fsuppind  39456  prjspnval2  39611  imaiinfv  39634  mapfzcons1  39658  rexrabdioph  39735  dnnumch1  39988  dnwech  39992  aomclem6  40003  pwssplit4  40033  pwfi2f1o  40040  mendplusgfval  40129  mendvscafval  40134  harval3  40244  dssmapntrcls  40831  scotteqd  40945  colleq12d  40961  uzmptshftfval  41050  dropab1  41151  dropab2  41152  rabbida2  41768  rabbida3  41771  itgsinexplem1  42596  wallispi2lem2  42714  fourierdlem36  42785  etransclem4  42880  afveq12d  43689  aoveq123d  43734  aovfundmoveq  43737  aovnuoveq  43747  aovvoveq  43748  aovovn0oveq  43750  afv2eq12d  43771  fsumsplitsndif  43890  rngccofvalALTV  44611  ringccofvalALTV  44674  rhmsubclem2  44711  rhmsubcALTVlem2  44729  itscnhlinecirc02plem2  45197  setrecseq  45215  aacllem  45329