Theorem 3eqtr4g 2799

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

Syntax hints:   → wi 4   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  rabbidva2  3434  rabbida4  3459  rabeqf  3469  csbeq1  3910  csbeq2  3912  csbeq2d  3913  csbeq2dv  3914  difeq1  4128  difeq2  4129  uneq2  4171  ineq1  4220  ineq2  4221  symdifeq1  4260  symdifeq2  4261  dfrab3ss  4328  csbprc  4414  csbnestgfw  4427  csbnestgf  4432  disjssun  4473  ifeq1  4534  ifeq2  4535  pweqALT  4619  sneq  4640  rabsneq  4648  csbsng  4712  csbprg  4713  preq1  4737  preq2  4738  tpeq1  4746  tpeq2  4747  tpeq3  4748  prprc1  4769  tpprceq3  4808  opeq1  4877  opeq2  4878  oteq1  4886  oteq2  4887  oteq3  4888  csbopg  4895  uniprg  4927  csbuni  4940  inteq  4953  iineq1  5013  iineq2  5016  iuneq12df  5022  iuneq12d  5025  dfiin2g  5036  iinrab  5073  iinin1  5083  iinxprg  5093  iununi  5103  opabbid  5212  opabbidv  5213  mpteq12da  5232  mpteq12dfOLD  5234  mpteq12f  5235  mpteq12dva  5236  csbmpt12  5566  xpeq1  5702  xpeq2  5709  rneq  5949  reseq1  5993  reseq2  5994  resima2  6035  resindm  6049  resmpt  6056  resmptf  6058  imaeq1  6074  imaeq2  6075  mptcnv  6161  xpdisj1  6182  xpdisj2  6183  resdisj  6190  dmpropg  6236  rnpropg  6243  cores  6270  cores2  6280  xpco  6310  predeq123  6323  csbpredg  6328  sspred  6331  predres  6361  suceq  6451  sucprc  6461  iotaeq  6527  iotabi  6528  fntpg  6627  imain  6652  f1oprswap  6892  fveq1  6905  fveq2  6906  fvres  6925  csbfv12  6954  fnimapr  6991  fnimatpd  6992  fvco2  7005  xpprsng  7159  residpr  7162  fsnunfv  7206  fsnunres  7207  funiunfv  7267  f1ofvswap  7325  fliftf  7334  isoini2  7358  eqfunressuc  7380  riotaeqdv  7388  riotabidv  7389  riotauni  7393  riotabidva  7406  snriota  7420  oveq  7436  oveq1  7437  oveq2  7438  oprabbid  7497  oprabbidv  7498  mpoeq123  7504  mpoeq123dva  7506  mpoeq3dva  7509  resmpo  7552  ovres  7598  f1ocnvd  7683  ofeqd  7698  ofreq  7700  fpar  8139  frecseq123  8305  csbfrecsg  8307  wrecseq123  8337  wrecseq123OLD  8338  csbwrecsg  8344  onovuni  8380  recseq  8412  tfr2a  8433  rdgeq1  8449  rdgeq2  8450  rdgsucmptf  8466  frsucmpt  8476  seqomeq12  8492  seqomsuc  8495  omopthi  8697  eceq1  8782  eceq2  8784  qseq1  8799  qseq2  8800  uniqs  8815  ecinxp  8830  qsinxp  8831  erovlem  8851  ecopovtrn  8858  ixpeq1  8946  unfi  9209  supeq1  9482  supeq2  9485  supeq3  9486  supeq123d  9487  infeq1  9513  infeq2  9516  infeq3  9517  infeq123d  9518  infiso  9545  oieq1  9549  oieq2  9550  ordtypelem1  9555  inf3lemc  9663  wemapwe  9734  ttrcleq  9746  r1sucg  9806  r1limg  9808  rankprb  9888  karden  9932  djueq12  9941  cardiun  10019  acneq  10080  alephlim  10104  alephsuc  10105  alephfplem2  10142  infpssrlem2  10341  fin23lem34  10383  fin23lem35  10384  zorn2lem1  10533  zorn2lem7  10539  fpwwe2lem5  10672  fpwwe2lem12  10679  addpiord  10921  mulpiord  10922  addpqnq  10975  mulpqnq  10978  addassnq  10995  mulassnq  10996  distrnq  10998  lterpq  11007  ltexnq  11012  ltsrpr  11114  00sr  11136  recexsrlem  11140  mulgt0sr  11142  addcnsrec  11180  mulcnsrec  11181  negeq  11497  csbnegg  11502  negsubdi  11562  mulneg1  11696  negfi  12214  deceq1  12735  deceq2  12736  xnegeq  13245  fseq1p1m1  13634  om2uzrdg  13993  uzrdgsuci  13997  seqeq1  14041  seqeq2  14042  seqeq3  14043  seqfeq4  14088  seqof  14096  hashprg  14430  hashtpg  14520  csbwrdg  14578  s1eq  14634  cats1co  14891  s2eqd  14898  s3eqd  14899  s4eqd  14900  s5eqd  14901  s6eqd  14902  s7eqd  14903  s8eqd  14904  xpcogend  15009  shftval  15109  limsupgle  15509  lo1eq  15600  rlimeq  15601  sumeq1  15721  sumeq2w  15724  sumeq2ii  15725  sumeq2sdv  15735  zsum  15750  sumss2  15758  fsumsplitsnun  15787  isumclim3  15791  fsumcom2  15806  incexclem  15868  incexc2  15870  isumshft  15871  prodeq1f  15938  prodeq1  15939  prodeq2w  15942  prodeq2ii  15943  prodeq2sdv  15955  zprod  15969  fprodm1s  16002  fprodp1s  16003  fprodcom2  16016  fprodsplitf  16020  iprodclim3  16032  ef0lem  16110  ruclem7  16268  sadcp1  16488  smupp1  16513  smueqlem  16523  algrp1  16607  dfphi2  16807  prmdiveq  16819  pceulem  16878  vdwlem6  17019  cshwsiun  17133  sloteq  17216  setsid  17241  elbasfv  17250  elbasov  17251  imastset  17568  imasvscaval  17584  isoval  17812  funcoppc  17925  fulloppc  17975  fuccofval  18014  natpropd  18032  catccofval  18157  xpchomfval  18234  xpccofval  18237  lubfval  18407  glbfval  18420  grpidpropd  18687  gsumpropd2lem  18704  frmdplusg  18879  efmndplusg  18905  grpinvpropd  19045  grpsubpropd  19075  grpsubpropd2  19076  mulgpropd  19146  ecqusaddd  19222  oppgmnd  19387  sylow1lem2  19631  sylow3lem1  19659  prds1  20336  pwsmgp  20340  opprrng  20361  rngidpropd  20431  dvdsrpropd  20432  unitpropd  20433  invrpropd  20434  rhm1  20505  rhmopp  20525  rhmsubclem2  20702  lmhmpropd  21089  lidlrsppropd  21271  rngqiprnglinlem2  21319  lpival  21351  pzriprnglem11  21519  zrhpropd  21542  znle  21568  frlmplusgval  21801  frlmvscafval  21803  ressascl  21933  asclpropd  21934  aspval2  21935  psrbas  21970  psrplusg  21973  psrmulr  21979  psrvscafval  21985  resspsrbas  22011  ressmplbas2  22062  opsrle  22082  opsrbaslem  22084  opsrbaslemOLD  22085  vr1val  22208  ressply1add  22246  ressply1mul  22247  ressply1vsca  22248  psrplusgpropd  22252  mplbaspropd  22253  psropprmul  22254  ply1baspropd  22259  ply1plusgpropd  22260  ply1sca2  22270  ply1ascl0  22271  ply1ascl1  22272  subrgvr1  22279  coe1mul2lem2  22286  ply1coe1eq  22319  evls1addd  22390  evls1muld  22391  evls1vsca  22392  rhmply1vr1  22406  rhmply1vsca  22407  mamudi  22422  mamudir  22423  matrcl  22431  oftpos  22473  mattpos1  22477  mdetfval  22607  mdetrlin  22623  mdetrsca  22624  mdetrsca2  22625  mdetrlin2  22628  mdetunilem5  22637  madufval  22658  madugsum  22664  idmatidpmat  22758  cpmidpmat  22894  cncmp  23415  2ndcsep  23482  llyeq  23493  nllyeq  23494  xkouni  23622  hmphindis  23820  xkocnv  23837  ptcmplem2  24076  snclseqg  24139  prdstmdd  24147  ustexsym  24239  ucnextcn  24328  metreslem  24387  comet  24541  nrmmetd  24602  nmpropd  24622  isngp3  24626  ngpds  24632  subgnm  24661  tngnm  24687  idnghm  24779  cnmetdval  24806  cnmpopc  24968  htpyco2  25024  phtpyco2  25035  clsocv  25297  rrxprds  25436  rrxnm  25438  rrxplusgvscavalb  25442  ovolunlem1a  25544  voliunlem3  25600  ioombl1lem4  25609  uniioombllem4  25634  itg11  25739  itgeq1f  25820  itgeq1fOLD  25821  itgeq1  25822  itgeq2  25827  iblss2  25855  itgss  25861  itgeqa  25863  itgfsum  25876  itgsplit  25885  ditgeq1  25897  ditgeq2  25898  ditgeq3  25899  dvcmulf  25996  dvmptfsum  26027  dvcnvrelem2  26071  mdegfval  26115  mdegpropd  26137  deg1propd  26139  plyeq0  26264  coe11  26306  dgrlt  26320  dgradd2  26322  dgrmulc  26325  dvply1  26339  fta1lem  26363  pserulm  26479  rlimcnp2  27023  jensenlem1  27044  basellem5  27142  dchrbas  27293  dchrrcl  27298  dchrplusg  27305  dchrfi  27313  lgsdi  27392  lgseisenlem2  27434  lgsquadlem3  27440  dchrmusumlema  27551  rpvmasum2  27570  dchrisum0lema  27572  pntlemg  27656  nosupbnd2lem1  27774  lruneq  27958  addsval  28009  mulsval  28149  seqseq123d  28306  colperpexlem2  28753  axlowdimlem13  28983  uhgrvtxedgiedgb  29167  nb3grprlem1  29411  crctcshlem2  29847  wpthswwlks2on  29990  clwlknf1oclwwlkn  30112  frgrncvvdeq  30337  avril1  30491  0vfval  30634  imsval  30713  imsdval  30714  bcseqi  31148  normpythi  31170  cm0  31637  fh1  31646  pjcji  31712  opsqrlem5  32172  pjsdi2i  32185  pjclem3  32225  pjci  32228  golem1  32299  iuneq12daf  32576  iunrdx  32583  ofresid  32658  cnvprop  32710  coprprop  32713  f1od2  32738  dp2eq1  32839  dp2eq2  32840  fzto1st1  33104  gsumvsca1  33214  gsumvsca2  33215  urpropd  33221  resv1r  33347  nsgqusf1olem2  33421  oppr2idl  33493  opprqus0g  33497  lindsunlem  33651  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  algextdeglem4  33725  crefeq  33805  rspectopn  33827  xrge0mulc1cn  33901  qqhval2  33944  esumeq12dvaf  34011  esumeq2  34016  esumf1o  34030  esumfzf  34049  esumss  34052  esumpfinvalf  34056  ofceq  34077  carsgclctunlem1  34298  itgeq12dv  34307  ccatmulgnn0dir  34535  breprexpnat  34627  bnj956  34768  bnj1385  34824  bnj96  34857  bnj548  34889  bnj553  34890  bnj554  34891  bnj602  34907  bnj18eq1  34919  bnj1234  35005  bnj1296  35013  bnj1318  35017  bnj1442  35041  bnj1450  35042  cvmliftlem5  35273  cvmliftlem10  35278  cvmlift2lem9  35295  cvmliftphtlem  35301  satfdm  35353  mthmpps  35566  rdgprc  35775  dfrdg2  35776  wsuceq123  35795  wlimeq12  35800  altopthsn  35942  altxpeq1  35954  altxpeq2  35955  ixpeq12dv  36198  prodeq12sdv  36200  itgeq12sdv  36201  ditgeq123dv  36203  cbvcsbdavw  36241  cbvcsbdavw2  36242  cbvrabdavw  36243  cbviundavw  36244  cbviindavw  36245  cbvopab1davw  36246  cbvopab2davw  36247  cbvopabdavw  36248  cbvmptdavw  36249  cbviotadavw  36251  cbvriotadavw  36252  cbvoprab1davw  36253  cbvoprab2davw  36254  cbvoprab3davw  36255  cbvoprab123davw  36256  cbvoprab12davw  36257  cbvoprab23davw  36258  cbvoprab13davw  36259  cbvixpdavw  36260  cbvsumdavw  36261  cbvproddavw  36262  cbvitgdavw  36263  cbvditgdavw  36264  cbvrabdavw2  36267  cbviundavw2  36268  cbviindavw2  36269  cbvmptdavw2  36270  cbvriotadavw2  36272  cbvmpodavw2  36273  cbvmpo1davw2  36274  cbvmpo2davw2  36275  cbvixpdavw2  36276  cbvsumdavw2  36277  cbvproddavw2  36278  cbvitgdavw2  36279  cbvditgdavw2  36280  ee7.2aOLD  36443  bj-sngleq  36949  bj-tageq  36958  bj-projeq  36974  bj-projval  36978  bj-1upleq  36981  bj-pr1eq  36984  bj-pr2eq  36998  bj-evaleq  37054  bj-imafv  37233  csbrecsg  37310  csbrdgg  37311  csboprabg  37312  csbmpo123  37313  finxpeq1  37368  finxpeq2  37369  csbfinxpg  37370  finxpreclem4  37376  cureq  37582  unceq  37583  uncov  37587  unccur  37589  finixpnum  37591  ptrest  37605  poimirlem3  37609  poimirlem9  37615  poimirlem15  37621  poimirlem16  37622  poimirlem26  37632  poimirlem27  37633  mbfposadd  37653  cnambfre  37654  iblabsnclem  37669  ftc1anclem1  37679  heiborlem4  37800  heiborlem6  37802  mpobi123f  38148  iineq12f  38150  mptbi12f  38152  eccnvepres  38261  uniqsALTV  38310  xrneq1  38358  xrneq2  38361  cosseq  38407  redundss3  38609  riotaclbgBAD  38935  toycom  38954  ldualvbase  39107  ldualfvadd  39109  ldualsca  39113  ldualsbase  39114  ldualsaddN  39115  ldualfvs  39117  ldual0  39128  ldual1  39129  ldualneg  39130  cdleme19f  40290  cdleme20m  40305  cdleme21k  40320  cdleme27b  40350  cdleme31so  40361  cdleme31sn  40362  cdleme31se  40364  cdleme31se2  40365  cdleme31sc  40366  cdleme31sde  40367  cdleme31fv  40372  cdleme40v  40451  cdleme43dN  40474  cdlemeg46ngfr  40500  ltrnco4  40721  tgrpbase  40728  tgrpopr  40729  erngbase  40783  erngfplus  40784  erngfmul  40787  erngbase-rN  40791  erngfplus-rN  40792  erngfmul-rN  40795  dvasca  40988  dvavbase  40995  dvafvadd  40996  dvafvsca  40998  tendocnv  41003  dvhsca  41064  dvhfplusr  41066  dvhvbase  41069  dvhfvadd  41073  dvhfvsca  41082  lcdvadd  41579  lcdsbase  41582  lcdsadd  41583  lcdvs  41585  lcd0  41590  lcd1  41591  lcdneg  41592  fsuppind  42576  imaiinfv  42680  mapfzcons1  42704  rexrabdioph  42781  dnnumch1  43032  dnwech  43036  aomclem6  43047  pwssplit4  43077  pwfi2f1o  43084  mendplusgfval  43169  mendvscafval  43174  harval3  43527  dssmapntrcls  44117  scotteqd  44232  colleq12d  44248  uzmptshftfval  44341  dropab1  44442  dropab2  44443  iineq12dv  45045  rabbida2  45071  rabbida3  45074  itgsinexplem1  45909  wallispi2lem2  46027  fourierdlem36  46098  etransclem4  46193  fcoreslem1  47012  afveq12d  47082  aoveq123d  47127  aovfundmoveq  47130  aovnuoveq  47140  aovvoveq  47141  aovovn0oveq  47143  afv2eq12d  47164  fsumsplitsndif  47297  rngccofvalALTV  48113  rhmsubcALTVlem2  48125  ringccofvalALTV  48147  itscnhlinecirc02plem2  48632  setrecseq  48915  aacllem  49031