Theorem 3eqtr4g 2805

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  rabbidva2  3445  rabbida4  3470  rabeqf  3480  csbeq1  3924  csbeq2  3926  csbeq2d  3927  csbeq2dv  3928  difeq1  4142  difeq2  4143  uneq2  4185  ineq1  4234  ineq2  4235  symdifeq1  4274  symdifeq2  4275  dfrab3ss  4342  csbprc  4432  csbnestgfw  4445  csbnestgf  4450  disjssun  4491  ifeq1  4552  ifeq2  4553  pweqALT  4637  sneq  4658  rabsneq  4666  csbsng  4733  csbprg  4734  preq1  4758  preq2  4759  tpeq1  4767  tpeq2  4768  tpeq3  4769  prprc1  4790  tpprceq3  4829  opeq1  4897  opeq2  4898  oteq1  4906  oteq2  4907  oteq3  4908  csbopg  4915  uniprg  4947  csbuni  4960  inteq  4973  iineq1  5032  iineq2  5035  iuneq12df  5041  iuneq12d  5044  dfiin2g  5055  iinrab  5092  iinin1  5102  iinxprg  5112  iununi  5122  opabbid  5231  opabbidv  5232  mpteq12da  5251  mpteq12dfOLD  5253  mpteq12f  5254  mpteq12dva  5255  csbmpt12  5576  xpeq1  5714  xpeq2  5721  rneq  5961  reseq1  6003  reseq2  6004  resima2  6045  resindm  6059  resmpt  6066  resmptf  6068  imaeq1  6084  imaeq2  6085  mptcnv  6171  xpdisj1  6192  xpdisj2  6193  resdisj  6200  dmpropg  6246  rnpropg  6253  cores  6280  cores2  6290  xpco  6320  predeq123  6333  csbpredg  6338  sspred  6341  predres  6371  suceq  6461  sucprc  6471  iotaeq  6538  iotabi  6539  fntpg  6638  imain  6663  f1oprswap  6906  fveq1  6919  fveq2  6920  fvres  6939  csbfv12  6968  fnimapr  7005  fnimatpd  7006  fvco2  7019  xpprsng  7174  residpr  7177  fsnunfv  7221  fsnunres  7222  funiunfv  7285  f1ofvswap  7342  fliftf  7351  isoini2  7375  eqfunressuc  7397  riotaeqdv  7405  riotabidv  7406  riotauni  7410  riotabidva  7424  snriota  7438  oveq  7454  oveq1  7455  oveq2  7456  oprabbid  7515  oprabbidv  7516  mpoeq123  7522  mpoeq123dva  7524  mpoeq3dva  7527  resmpo  7570  ovres  7616  f1ocnvd  7701  ofeqd  7716  ofreq  7718  fpar  8157  frecseq123  8323  csbfrecsg  8325  wrecseq123  8355  wrecseq123OLD  8356  csbwrecsg  8362  onovuni  8398  recseq  8430  tfr2a  8451  rdgeq1  8467  rdgeq2  8468  rdgsucmptf  8484  frsucmpt  8494  seqomeq12  8510  seqomsuc  8513  omopthi  8717  eceq1  8802  eceq2  8804  qseq1  8819  qseq2  8820  uniqs  8835  ecinxp  8850  qsinxp  8851  erovlem  8871  ecopovtrn  8878  ixpeq1  8966  unfi  9238  supeq1  9514  supeq2  9517  supeq3  9518  supeq123d  9519  infeq1  9545  infeq2  9548  infeq3  9549  infeq123d  9550  infiso  9577  oieq1  9581  oieq2  9582  ordtypelem1  9587  inf3lemc  9695  wemapwe  9766  ttrcleq  9778  r1sucg  9838  r1limg  9840  rankprb  9920  karden  9964  djueq12  9973  cardiun  10051  acneq  10112  alephlim  10136  alephsuc  10137  alephfplem2  10174  infpssrlem2  10373  fin23lem34  10415  fin23lem35  10416  zorn2lem1  10565  zorn2lem7  10571  fpwwe2lem5  10704  fpwwe2lem12  10711  addpiord  10953  mulpiord  10954  addpqnq  11007  mulpqnq  11010  addassnq  11027  mulassnq  11028  distrnq  11030  lterpq  11039  ltexnq  11044  ltsrpr  11146  00sr  11168  recexsrlem  11172  mulgt0sr  11174  addcnsrec  11212  mulcnsrec  11213  negeq  11528  csbnegg  11533  negsubdi  11592  mulneg1  11726  negfi  12244  deceq1  12763  deceq2  12764  xnegeq  13269  fseq1p1m1  13658  om2uzrdg  14007  uzrdgsuci  14011  seqeq1  14055  seqeq2  14056  seqeq3  14057  seqfeq4  14102  seqof  14110  hashprg  14444  hashtpg  14534  csbwrdg  14592  s1eq  14648  cats1co  14905  s2eqd  14912  s3eqd  14913  s4eqd  14914  s5eqd  14915  s6eqd  14916  s7eqd  14917  s8eqd  14918  xpcogend  15023  shftval  15123  limsupgle  15523  lo1eq  15614  rlimeq  15615  sumeq1  15737  sumeq2w  15740  sumeq2ii  15741  sumeq2sdv  15751  zsum  15766  sumss2  15774  fsumsplitsnun  15803  isumclim3  15807  fsumcom2  15822  incexclem  15884  incexc2  15886  isumshft  15887  prodeq1f  15954  prodeq1  15955  prodeq2w  15958  prodeq2ii  15959  prodeq2sdv  15971  zprod  15985  fprodm1s  16018  fprodp1s  16019  fprodcom2  16032  fprodsplitf  16036  iprodclim3  16048  ef0lem  16126  ruclem7  16284  sadcp1  16501  smupp1  16526  smueqlem  16536  algrp1  16621  dfphi2  16821  prmdiveq  16833  pceulem  16892  vdwlem6  17033  cshwsiun  17147  sloteq  17230  setsid  17255  elbasfv  17264  elbasov  17265  imastset  17582  imasvscaval  17598  isoval  17826  funcoppc  17939  fulloppc  17989  fuccofval  18028  natpropd  18046  catccofval  18171  xpchomfval  18248  xpccofval  18251  lubfval  18420  glbfval  18433  grpidpropd  18700  gsumpropd2lem  18717  frmdplusg  18889  efmndplusg  18915  grpinvpropd  19055  grpsubpropd  19085  grpsubpropd2  19086  mulgpropd  19156  ecqusaddd  19232  oppgmnd  19397  sylow1lem2  19641  sylow3lem1  19669  prds1  20346  pwsmgp  20350  opprrng  20371  rngidpropd  20441  dvdsrpropd  20442  unitpropd  20443  invrpropd  20444  rhm1  20515  rhmopp  20535  rhmsubclem2  20708  lmhmpropd  21095  lidlrsppropd  21277  rngqiprnglinlem2  21325  lpival  21357  pzriprnglem11  21525  zrhpropd  21548  znle  21574  frlmplusgval  21807  frlmvscafval  21809  ressascl  21939  asclpropd  21940  aspval2  21941  psrbas  21976  psrplusg  21979  psrmulr  21985  psrvscafval  21991  resspsrbas  22017  ressmplbas2  22068  opsrle  22088  opsrbaslem  22090  opsrbaslemOLD  22091  vr1val  22214  ressply1add  22252  ressply1mul  22253  ressply1vsca  22254  psrplusgpropd  22258  mplbaspropd  22259  psropprmul  22260  ply1baspropd  22265  ply1plusgpropd  22266  ply1sca2  22276  ply1ascl0  22277  ply1ascl1  22278  subrgvr1  22285  coe1mul2lem2  22292  ply1coe1eq  22325  evls1addd  22396  evls1muld  22397  evls1vsca  22398  rhmply1vr1  22412  rhmply1vsca  22413  mamudi  22428  mamudir  22429  matrcl  22437  oftpos  22479  mattpos1  22483  mdetfval  22613  mdetrlin  22629  mdetrsca  22630  mdetrsca2  22631  mdetrlin2  22634  mdetunilem5  22643  madufval  22664  madugsum  22670  idmatidpmat  22764  cpmidpmat  22900  cncmp  23421  2ndcsep  23488  llyeq  23499  nllyeq  23500  xkouni  23628  hmphindis  23826  xkocnv  23843  ptcmplem2  24082  snclseqg  24145  prdstmdd  24153  ustexsym  24245  ucnextcn  24334  metreslem  24393  comet  24547  nrmmetd  24608  nmpropd  24628  isngp3  24632  ngpds  24638  subgnm  24667  tngnm  24693  idnghm  24785  cnmetdval  24812  cnmpopc  24974  htpyco2  25030  phtpyco2  25041  clsocv  25303  rrxprds  25442  rrxnm  25444  rrxplusgvscavalb  25448  ovolunlem1a  25550  voliunlem3  25606  ioombl1lem4  25615  uniioombllem4  25640  itg11  25745  itgeq1f  25826  itgeq1fOLD  25827  itgeq1  25828  itgeq2  25833  iblss2  25861  itgss  25867  itgeqa  25869  itgfsum  25882  itgsplit  25891  ditgeq1  25903  ditgeq2  25904  ditgeq3  25905  dvcmulf  26002  dvmptfsum  26033  dvcnvrelem2  26077  mdegfval  26121  mdegpropd  26143  deg1propd  26145  plyeq0  26270  coe11  26312  dgrlt  26326  dgradd2  26328  dgrmulc  26331  dvply1  26343  fta1lem  26367  pserulm  26483  rlimcnp2  27027  jensenlem1  27048  basellem5  27146  dchrbas  27297  dchrrcl  27302  dchrplusg  27309  dchrfi  27317  lgsdi  27396  lgseisenlem2  27438  lgsquadlem3  27444  dchrmusumlema  27555  rpvmasum2  27574  dchrisum0lema  27576  pntlemg  27660  nosupbnd2lem1  27778  lruneq  27962  addsval  28013  mulsval  28153  seqseq123d  28310  colperpexlem2  28757  axlowdimlem13  28987  uhgrvtxedgiedgb  29171  nb3grprlem1  29415  crctcshlem2  29851  wpthswwlks2on  29994  clwlknf1oclwwlkn  30116  frgrncvvdeq  30341  avril1  30495  0vfval  30638  imsval  30717  imsdval  30718  bcseqi  31152  normpythi  31174  cm0  31641  fh1  31650  pjcji  31716  opsqrlem5  32176  pjsdi2i  32189  pjclem3  32229  pjci  32232  golem1  32303  iuneq12daf  32579  iunrdx  32586  ofresid  32661  cnvprop  32708  coprprop  32711  f1od2  32735  dp2eq1  32837  dp2eq2  32838  fzto1st1  33095  gsumvsca1  33205  gsumvsca2  33206  urpropd  33212  resv1r  33333  nsgqusf1olem2  33407  oppr2idl  33479  opprqus0g  33483  lindsunlem  33637  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  algextdeglem4  33711  crefeq  33791  rspectopn  33813  xrge0mulc1cn  33887  qqhval2  33928  esumeq12dvaf  33995  esumeq2  34000  esumf1o  34014  esumfzf  34033  esumss  34036  esumpfinvalf  34040  ofceq  34061  carsgclctunlem1  34282  itgeq12dv  34291  ccatmulgnn0dir  34519  breprexpnat  34611  bnj956  34752  bnj1385  34808  bnj96  34841  bnj548  34873  bnj553  34874  bnj554  34875  bnj602  34891  bnj18eq1  34903  bnj1234  34989  bnj1296  34997  bnj1318  35001  bnj1442  35025  bnj1450  35026  cvmliftlem5  35257  cvmliftlem10  35262  cvmlift2lem9  35279  cvmliftphtlem  35285  satfdm  35337  mthmpps  35550  rdgprc  35758  dfrdg2  35759  wsuceq123  35778  wlimeq12  35783  altopthsn  35925  altxpeq1  35937  altxpeq2  35938  ixpeq12dv  36182  prodeq12sdv  36184  itgeq12sdv  36185  ditgeq123dv  36187  cbvcsbdavw  36225  cbvcsbdavw2  36226  cbvrabdavw  36227  cbviundavw  36228  cbviindavw  36229  cbvopab1davw  36230  cbvopab2davw  36231  cbvopabdavw  36232  cbvmptdavw  36233  cbviotadavw  36235  cbvriotadavw  36236  cbvoprab1davw  36237  cbvoprab2davw  36238  cbvoprab3davw  36239  cbvoprab123davw  36240  cbvoprab12davw  36241  cbvoprab23davw  36242  cbvoprab13davw  36243  cbvixpdavw  36244  cbvsumdavw  36245  cbvproddavw  36246  cbvitgdavw  36247  cbvditgdavw  36248  cbvrabdavw2  36251  cbviundavw2  36252  cbviindavw2  36253  cbvmptdavw2  36254  cbvriotadavw2  36256  cbvmpodavw2  36257  cbvmpo1davw2  36258  cbvmpo2davw2  36259  cbvixpdavw2  36260  cbvsumdavw2  36261  cbvproddavw2  36262  cbvitgdavw2  36263  cbvditgdavw2  36264  ee7.2aOLD  36427  bj-sngleq  36933  bj-tageq  36942  bj-projeq  36958  bj-projval  36962  bj-1upleq  36965  bj-pr1eq  36968  bj-pr2eq  36982  bj-evaleq  37038  bj-imafv  37217  csbrecsg  37294  csbrdgg  37295  csboprabg  37296  csbmpo123  37297  finxpeq1  37352  finxpeq2  37353  csbfinxpg  37354  finxpreclem4  37360  cureq  37556  unceq  37557  uncov  37561  unccur  37563  finixpnum  37565  ptrest  37579  poimirlem3  37583  poimirlem9  37589  poimirlem15  37595  poimirlem16  37596  poimirlem26  37606  poimirlem27  37607  mbfposadd  37627  cnambfre  37628  iblabsnclem  37643  ftc1anclem1  37653  heiborlem4  37774  heiborlem6  37776  mpobi123f  38122  iineq12f  38124  mptbi12f  38126  eccnvepres  38236  uniqsALTV  38285  xrneq1  38333  xrneq2  38336  cosseq  38382  redundss3  38584  riotaclbgBAD  38910  toycom  38929  ldualvbase  39082  ldualfvadd  39084  ldualsca  39088  ldualsbase  39089  ldualsaddN  39090  ldualfvs  39092  ldual0  39103  ldual1  39104  ldualneg  39105  cdleme19f  40265  cdleme20m  40280  cdleme21k  40295  cdleme27b  40325  cdleme31so  40336  cdleme31sn  40337  cdleme31se  40339  cdleme31se2  40340  cdleme31sc  40341  cdleme31sde  40342  cdleme31fv  40347  cdleme40v  40426  cdleme43dN  40449  cdlemeg46ngfr  40475  ltrnco4  40696  tgrpbase  40703  tgrpopr  40704  erngbase  40758  erngfplus  40759  erngfmul  40762  erngbase-rN  40766  erngfplus-rN  40767  erngfmul-rN  40770  dvasca  40963  dvavbase  40970  dvafvadd  40971  dvafvsca  40973  tendocnv  40978  dvhsca  41039  dvhfplusr  41041  dvhvbase  41044  dvhfvadd  41048  dvhfvsca  41057  lcdvadd  41554  lcdsbase  41557  lcdsadd  41558  lcdvs  41560  lcd0  41565  lcd1  41566  lcdneg  41567  fsuppind  42545  imaiinfv  42649  mapfzcons1  42673  rexrabdioph  42750  dnnumch1  43001  dnwech  43005  aomclem6  43016  pwssplit4  43046  pwfi2f1o  43053  mendplusgfval  43142  mendvscafval  43147  harval3  43500  dssmapntrcls  44090  scotteqd  44206  colleq12d  44222  uzmptshftfval  44315  dropab1  44416  dropab2  44417  iineq12dv  45008  rabbida2  45034  rabbida3  45037  itgsinexplem1  45875  wallispi2lem2  45993  fourierdlem36  46064  etransclem4  46159  fcoreslem1  46978  afveq12d  47048  aoveq123d  47093  aovfundmoveq  47096  aovnuoveq  47106  aovvoveq  47107  aovovn0oveq  47109  afv2eq12d  47130  fsumsplitsndif  47247  rngccofvalALTV  47993  rhmsubcALTVlem2  48005  ringccofvalALTV  48027  itscnhlinecirc02plem2  48517  setrecseq  48777  aacllem  48895