Theorem 3eqtr4g 2820

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752

This theorem is used by:  rabbidva2  3414  rabbida4  3436  csbeq1  3850  csbeq2  3852  csbeq2d  3853  csbeq2dv  3854  difeq1  4067  difeq2  4068  uneq2  4109  ineq1  4159  ineq2  4160  symdifeq1  4201  symdifeq2  4202  dfrab3ss  4269  csbprc  4367  csbnestgfw  4380  csbnestgf  4385  disjssun  4421  ifeq1  4486  ifeq2  4487  pweqALT  4572  sneq  4594  csbsng  4669  csbprg  4670  preq1  4694  preq2  4695  tpeq1  4703  tpeq2  4704  tpeq3  4705  prprc1  4726  tpprceq3  4767  opeq1  4833  opeq2  4834  oteq1  4842  oteq2  4843  oteq3  4844  csbopg  4851  uniprg  4883  csbuni  4898  inteq  4910  iineq1  4969  iineq2  4972  iuneq12df  4978  iuneq12d  4980  dfiin2g  4989  iinrab  5027  iinin1  5039  iinxprg  5049  iununi  5059  opabbid  5170  opabbidv  5171  mpteq12da  5188  mpteq12f  5190  mpteq12dva  5191  csbmpt12  5536  xpeq1  5669  xpeq2  5676  rneq  5920  reseq1  5966  reseq2  5967  resima2  6009  resindmOLD  6024  resmpt  6033  resmptf  6035  imaeq1  6051  imaeq2  6052  mptcnv  6132  xpdisj1  6153  xpdisj2  6154  resdisj  6162  dmpropg  6211  rnpropg  6218  cores  6245  cores2  6256  xpco  6287  predeq123  6300  csbpredg  6305  sspred  6308  predres  6337  suceqd  6425  sucprc  6436  iotaeq  6501  iotabi  6502  fntpg  6594  imain  6619  f1oprswap  6864  fveq1  6878  fveq2  6879  fvres  6898  csbfv12  6924  fnimapr  6962  fnimatpd  6963  fvco2  6976  xpprsng  7136  xpsnprg  7137  xpsntpg  7138  residpr  7140  fsnunfv  7186  fsnunres  7187  funiunfv  7246  f1ofvswap  7308  fliftf  7317  isoini2  7341  eqfunressuc  7365  riotaeqdv  7372  riotabidv  7373  riotauni  7377  riotabidva  7390  snriota  7404  oveq  7420  oveq1  7421  oveq2  7422  oprabbid  7479  oprabbidv  7480  mpoeq123  7486  mpoeq123dva  7488  mpoeq3dva  7491  resmpo  7534  ovres  7580  f1ocnvd  7666  ofeqd  7681  ofreq  7683  fpar  8114  frecseq123  8282  csbfrecsg  8284  wrecseq123  8313  csbwrecsg  8318  onovuni  8332  recseq  8363  tfr2a  8385  rdgeq1  8401  rdgeq2  8402  rdgsucmptf  8418  frsucmpt  8428  seqomeq12  8446  seqomsuc  8449  omopthi  8652  eceq1  8739  eceq2  8741  qseq1  8759  qseq2  8760  uniqs  8776  snecg  8780  ecinxp  8795  qsinxp  8796  erovlem  8816  ecopovtrn  8823  cureq  8871  uncov  8875  ixpeq1  8918  unfi  9168  supeq1  9418  supeq2  9421  supeq3  9422  supeq123d  9423  infeq1  9450  infeq2  9453  infeq3  9454  infeq123d  9455  infiso  9483  oieq1  9487  oieq2  9488  ordtypelem1  9493  inf3lemc  9608  wemapwe  9679  ttrcleq  9691  r1sucg  9754  r1limg  9756  rankprb  9836  scotteqd  9872  karden  9901  kardenOLD  9902  djueq12  9912  cardiun  9990  acneq  10049  alephlim  10073  alephsuc  10074  alephfplem2  10111  infpssrlem2  10309  fin23lem34  10351  fin23lem35  10352  zorn2lem1  10501  zorn2lem7  10507  fpwwe2lem5  10647  fpwwe2lem12  10654  addpiord  10896  mulpiord  10897  addpqnq  10950  mulpqnq  10953  addassnq  10970  mulassnq  10971  distrnq  10973  lterpq  10982  ltexnq  10987  ltsrpr  11089  00sr  11111  recexsrlem  11115  mulgt0sr  11117  addcnsrec  11155  mulcnsrec  11156  negeq  11476  csbnegg  11481  negsubdi  11541  mulneg1  11677  negfi  12191  deceq1  12744  deceq2  12745  xnegeq  13262  fseq1p1m1  13656  om2uzrdg  14023  uzrdgsuci  14027  seqeq1  14071  seqeq2  14072  seqeq3  14073  seqfeq4  14118  seqof  14126  hashprg  14462  hashtpg  14553  csbwrdg  14612  s1eq  14670  cats1co  14930  s2eqd  14937  s3eqd  14938  s4eqd  14939  s5eqd  14940  s6eqd  14941  s7eqd  14942  s8eqd  14943  xpcogend  15050  shftval  15150  limsupgle  15567  lo1eq  15658  rlimeq  15659  sumeq1  15779  sumeq2w  15782  sumeq2ii  15783  sumeq2sdv  15793  zsum  15807  sumss2  15815  fsumsplitsnun  15844  isumclim3  15848  fsumcom2  15863  incexclem  15928  incexc2  15930  isumshft  15931  prodeq1f  15998  prodeq1  15999  prodeq2w  16002  prodeq2ii  16003  prodeq2sdv  16014  zprod  16027  fprodm1s  16060  fprodp1s  16061  fprodcom2  16074  fprodsplitf  16078  iprodclim3  16090  ef0lem  16167  ruclem7  16327  sadcp1  16548  smupp1  16573  smueqlem  16583  algrp1  16667  dfphi2  16868  prmdiveq  16880  pceulem  16940  vdwlem6  17081  cshwsiun  17194  sloteq  17278  setsid  17302  elbasfv  17310  elbasov  17311  imastset  17611  imasvscaval  17627  isoval  17857  funcoppc  17967  fulloppc  18016  fuccofval  18054  natpropd  18071  catccofval  18196  xpchomfval  18270  xpccofval  18273  lubfval  18439  glbfval  18452  chneq1  18703  chneq2  18704  grpidpropd  18758  gsumpropd2lem  18784  frmdplusg  18966  efmndplusg  18992  grpinvpropd  19141  grpsubpropd  19171  grpsubpropd2  19172  mulgpropd  19242  ecqusaddd  19323  oppgmnd  19484  sylow1lem2  19729  sylow3lem1  19757  prds1  20466  pwsmgp  20470  opprrng  20489  rngidpropd  20559  dvdsrpropd  20560  unitpropd  20561  invrpropd  20562  rhm1  20638  rhmopp  20672  rhmsubclem2  20851  lmhmpropd  21260  lidlrsppropd  21444  rngqiprnglinlem2  21498  lpival  21558  pzriprnglem11  21707  zrhpropd  21730  znle  21752  frlmplusgval  21980  frlmvscafval  21982  ressascl  22114  asclpropd  22115  aspval2  22116  psrbas  22152  psrplusg  22155  psrmulr  22160  psrvscafval  22166  resspsrbas  22191  ressmplbas2  22245  opsrle  22266  opsrbaslem  22268  vr1val  22420  ressply1add  22457  ressply1mul  22458  ressply1vsca  22459  psrplusgpropd  22463  mplbaspropd  22464  psropprmul  22465  ply1baspropd  22470  ply1plusgpropd  22471  ply1sca2  22481  ply1ascl0  22482  ply1ascl1  22483  subrgvr1  22490  coe1mul2lem2  22497  ply1coe1eq  22528  evls1addd  22599  evls1muld  22600  evls1vsca  22601  rhmply1vr1  22612  rhmply1vsca  22613  mamudi  22628  mamudir  22629  matrcl  22637  oftpos  22677  mattpos1  22681  mdetfval  22811  mdetrlin  22827  mdetrsca  22828  mdetrsca2  22829  mdetrlin2  22832  mdetunilem5  22841  madufval  22862  madugsum  22868  idmatidpmat  22965  cpmidpmat  23101  cncmp  23620  2ndcsep  23688  llyeq  23699  nllyeq  23700  xkouni  23828  hmphindis  24026  xkocnv  24043  ptcmplem2  24282  snclseqg  24345  prdstmdd  24353  ustexsym  24445  ucnextcn  24532  metreslem  24591  comet  24742  nrmmetd  24803  nmpropd  24823  isngp3  24827  ngpds  24833  subgnm  24862  tngnm  24880  idnghm  24972  cnmetdval  24999  cnmpopc  25159  htpyco2  25210  phtpyco2  25221  clsocv  25481  rrxprds  25620  rrxnm  25622  rrxplusgvscavalb  25626  ovolunlem1a  25727  voliunlem3  25783  ioombl1lem4  25792  uniioombllem4  25817  itg11  25922  itgeq1f  26002  itgeq1  26003  itgeq2  26008  iblss2  26036  itgss  26042  itgeqa  26044  itgfsum  26057  itgsplit  26066  ditgeq1  26078  ditgeq2  26079  ditgeq3  26080  dvcmulf  26175  dvmptfsum  26205  dvcnvrelem2  26248  mdegfval  26290  mdegpropd  26312  deg1propd  26314  plyeq0  26440  coe11  26482  dgrlt  26495  dgradd2  26497  dgrmulc  26500  dvply1  26517  fta1lem  26540  pserulm  26661  rlimcnp2  27206  jensenlem1  27226  basellem5  27324  dchrbas  27474  dchrrcl  27479  dchrplusg  27486  dchrfi  27494  lgsdi  27573  lgseisenlem2  27615  lgsquadlem3  27621  dchrmusumlema  27732  rpvmasum2  27751  dchrisum0lema  27753  pntlemg  27837  nosupbnd2lem1  27954  lruneq  28175  addsval  28230  mulsval  28377  seqseq123d  28554  colperpexlem2  29089  symquadmid  29186  tgaaddcpbllem2  29232  axlowdimlem13  29414  uhgrvtxedgiedgb  29596  nb3grprlem1  29843  crctcshlem2  30289  wpthswwlks2on  30435  clwlknf1oclwwlkn  30557  frgrncvvdeq  30792  avril1  30946  0vfval  31090  imsval  31169  imsdval  31170  bcseqi  31604  normpythi  31626  cm0  32093  fh1  32102  pjcji  32168  opsqrlem5  32628  pjsdi2i  32641  pjclem3  32681  pjci  32684  golem1  32755  iuneq12daf  33033  iunrdx  33040  ofresid  33118  cnvprop  33171  coprprop  33174  f1od2  33193  dp2eq1  33321  dp2eq2  33322  fzto1st1  33545  gsumvsca1  33669  gsumvsca2  33670  urpropd  33673  resv1r  33782  nsgqusf1olem2  33846  oppr2idl  33891  opprqus0g  33895  ressply1evls1  33978  esplyfvn  34090  vietalem  34092  lindsunlem  34137  fedgmullem1  34142  fedgmullem2  34143  fedgmul  34144  fldsdrgfldext2  34175  fldextrspunlem1  34188  fldextrspunfld  34189  algextdeglem4  34233  crefeq  34358  rspectopn  34380  xrge0mulc1cn  34454  qqhval2  34495  esumeq12dvaf  34544  esumeq2  34549  esumf1o  34563  esumfzf  34582  esumss  34585  esumpfinvalf  34589  ofceq  34610  carsgclctunlem1  34831  itgeq12dv  34840  ccatmulgnn0dir  35056  breprexpnat  35145  bnj956  35289  bnj1385  35344  bnj96  35377  bnj548  35409  bnj553  35410  bnj554  35411  bnj602  35427  bnj18eq1  35439  bnj1234  35525  bnj1296  35533  bnj1318  35537  bnj1442  35561  bnj1450  35562  cvmliftlem5  35871  cvmliftlem10  35876  cvmlift2lem9  35893  cvmliftphtlem  35899  satfdm  35951  mthmpps  36164  rdgprc  36374  dfrdg2  36375  wsuceq123  36394  wlimeq12  36399  altopthsn  36544  altxpeq1  36556  altxpeq2  36557  nmulprop  36773  ixpeq12dv  36839  prodeq12sdv  36841  itgeq12sdv  36842  ditgeq123dv  36844  cbvcsbdavw  36882  cbvcsbdavw2  36883  cbvrabdavw  36884  cbviundavw  36885  cbviindavw  36886  cbvopab1davw  36887  cbvopab2davw  36888  cbvopabdavw  36889  cbvmptdavw  36890  cbviotadavw  36892  cbvriotadavw  36893  cbvoprab1davw  36894  cbvoprab2davw  36895  cbvoprab3davw  36896  cbvoprab123davw  36897  cbvoprab12davw  36898  cbvoprab23davw  36899  cbvoprab13davw  36900  cbvixpdavw  36901  cbvsumdavw  36902  cbvproddavw  36903  cbvitgdavw  36904  cbvditgdavw  36905  cbvrabdavw2  36908  cbviundavw2  36909  cbviindavw2  36910  cbvmptdavw2  36911  cbvriotadavw2  36913  cbvmpodavw2  36914  cbvmpo1davw2  36915  cbvmpo2davw2  36916  cbvixpdavw2  36917  cbvsumdavw2  36918  cbvproddavw2  36919  cbvitgdavw2  36920  cbvditgdavw2  36921  ee7.2aOLD  37083  ttceq  37110  bj-sngleq  37714  bj-tageq  37723  bj-projeq  37739  bj-projval  37743  bj-1upleq  37746  bj-pr1eq  37749  bj-pr2eq  37763  bj-evaleq  37824  bj-imafv  38006  csbrecsg  38085  csbrdgg  38086  csboprabg  38087  csbmpo123  38088  finxpeq1  38143  finxpeq2  38144  csbfinxpg  38145  finxpreclem4  38151  unceq  38358  unccur  38360  finixpnum  38362  ptrest  38371  poimirlem3  38375  poimirlem9  38381  poimirlem15  38387  poimirlem16  38388  poimirlem26  38398  poimirlem27  38399  mbfposadd  38419  cnambfre  38420  iblabsnclem  38435  ftc1anclem1  38445  heiborlem4  38567  heiborlem6  38569  mpobi123f  38913  iineq12f  38915  mptbi12f  38917  eccnvepres  39037  xrneq1  39147  xrneq2  39150  shiftstableeq2  39234  cosseq  39267  redundss3  39463  riotaclbgBAD  39830  toycom  39849  ldualvbase  40002  ldualfvadd  40004  ldualsca  40008  ldualsbase  40009  ldualsaddN  40010  ldualfvs  40012  ldual0  40023  ldual1  40024  ldualneg  40025  cdleme19f  41184  cdleme20m  41199  cdleme21k  41214  cdleme27b  41244  cdleme31so  41255  cdleme31sn  41256  cdleme31se  41258  cdleme31se2  41259  cdleme31sc  41260  cdleme31sde  41261  cdleme31fv  41266  cdleme40v  41345  cdleme43dN  41368  cdlemeg46ngfr  41394  ltrnco4  41615  tgrpbase  41622  tgrpopr  41623  erngbase  41677  erngfplus  41678  erngfmul  41681  erngbase-rN  41685  erngfplus-rN  41686  erngfmul-rN  41689  dvasca  41882  dvavbase  41889  dvafvadd  41890  dvafvsca  41892  tendocnv  41897  dvhsca  41958  dvhfplusr  41960  dvhvbase  41963  dvhfvadd  41967  dvhfvsca  41976  lcdvadd  42473  lcdsbase  42476  lcdsadd  42477  lcdvs  42479  lcd0  42484  lcd1  42485  lcdneg  42486  fsuppind  43439  imaiinfv  43541  mapfzcons1  43565  rexrabdioph  43638  dnnumch1  43888  dnwech  43892  aomclem6  43903  pwssplit4  43933  pwfi2f1o  43940  mendplusgfval  44025  mendvscafval  44030  harval3  44381  dssmapntrcls  44971  colleq12d  45080  uzmptshftfval  45173  dropab1  45273  dropab2  45274  iineq12dv  45941  rabbida2  45967  rabbida3  45970  itgsinexplem1  46785  wallispi2lem2  46903  fourierdlem36  46974  etransclem4  47069  fcoreslem1  47954  afveq12d  48024  aoveq123d  48069  aovfundmoveq  48072  aovnuoveq  48082  aovvoveq  48083  aovovn0oveq  48085  afv2eq12d  48106  fsumsplitsndif  48272  rngccofvalALTV  49188  rhmsubcALTVlem2  49200  ringccofvalALTV  49222  itscnhlinecirc02plem2  49716  oppfrcl3  50059  oppf1st2nd  50060  uppropd  50110  natoppf  50158  catcrcl  50324  lmdpropd  50586  cmdpropd  50587  lmddu  50596  cmddu  50597  setrecseq  50614  aacllem  50775