Theorem 3eqtr4g 2789

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  rabbidva2  3407  rabbida4  3431  rabeqf  3440  csbeq1  3865  csbeq2  3867  csbeq2d  3868  csbeq2dv  3869  difeq1  4082  difeq2  4083  uneq2  4125  ineq1  4176  ineq2  4177  symdifeq1  4218  symdifeq2  4219  dfrab3ss  4286  csbprc  4372  csbnestgfw  4385  csbnestgf  4390  disjssun  4431  ifeq1  4492  ifeq2  4493  pweqALT  4578  sneq  4599  rabsneq  4608  csbsng  4672  csbprg  4673  preq1  4697  preq2  4698  tpeq1  4706  tpeq2  4707  tpeq3  4708  prprc1  4729  tpprceq3  4768  opeq1  4837  opeq2  4838  oteq1  4846  oteq2  4847  oteq3  4848  csbopg  4855  uniprg  4887  csbuni  4900  inteq  4913  iineq1  4973  iineq2  4976  iuneq12df  4982  iuneq12d  4985  dfiin2g  4996  iinrab  5033  iinin1  5043  iinxprg  5053  iununi  5063  opabbid  5172  opabbidv  5173  mpteq12da  5190  mpteq12f  5192  mpteq12dva  5193  csbmpt12  5517  xpeq1  5652  xpeq2  5659  rneq  5900  reseq1  5944  reseq2  5945  resima2  5987  resindm  6001  resmpt  6008  resmptf  6010  imaeq1  6026  imaeq2  6027  mptcnv  6112  xpdisj1  6134  xpdisj2  6135  resdisj  6142  dmpropg  6188  rnpropg  6195  cores  6222  cores2  6232  xpco  6262  predeq123  6275  csbpredg  6280  sspred  6283  predres  6312  suceqd  6399  sucprc  6410  iotaeq  6476  iotabi  6477  fntpg  6576  imain  6601  f1oprswap  6844  fveq1  6857  fveq2  6858  fvres  6877  csbfv12  6906  fnimapr  6944  fnimatpd  6945  fvco2  6958  xpprsng  7112  residpr  7115  fsnunfv  7161  fsnunres  7162  funiunfv  7222  f1ofvswap  7281  fliftf  7290  isoini2  7314  eqfunressuc  7336  riotaeqdv  7345  riotabidv  7346  riotauni  7350  riotabidva  7363  snriota  7377  oveq  7393  oveq1  7394  oveq2  7395  oprabbid  7454  oprabbidv  7455  mpoeq123  7461  mpoeq123dva  7463  mpoeq3dva  7466  resmpo  7509  ovres  7555  f1ocnvd  7640  ofeqd  7655  ofreq  7657  fpar  8095  frecseq123  8261  csbfrecsg  8263  wrecseq123  8292  csbwrecsg  8297  onovuni  8311  recseq  8342  tfr2a  8363  rdgeq1  8379  rdgeq2  8380  rdgsucmptf  8396  frsucmpt  8406  seqomeq12  8422  seqomsuc  8425  omopthi  8625  eceq1  8710  eceq2  8712  qseq1  8730  qseq2  8731  uniqs  8747  ecinxp  8765  qsinxp  8766  erovlem  8786  ecopovtrn  8793  ixpeq1  8881  unfi  9135  supeq1  9396  supeq2  9399  supeq3  9400  supeq123d  9401  infeq1  9428  infeq2  9431  infeq3  9432  infeq123d  9433  infiso  9461  oieq1  9465  oieq2  9466  ordtypelem1  9471  inf3lemc  9579  wemapwe  9650  ttrcleq  9662  r1sucg  9722  r1limg  9724  rankprb  9804  karden  9848  djueq12  9857  cardiun  9935  acneq  9996  alephlim  10020  alephsuc  10021  alephfplem2  10058  infpssrlem2  10257  fin23lem34  10299  fin23lem35  10300  zorn2lem1  10449  zorn2lem7  10455  fpwwe2lem5  10588  fpwwe2lem12  10595  addpiord  10837  mulpiord  10838  addpqnq  10891  mulpqnq  10894  addassnq  10911  mulassnq  10912  distrnq  10914  lterpq  10923  ltexnq  10928  ltsrpr  11030  00sr  11052  recexsrlem  11056  mulgt0sr  11058  addcnsrec  11096  mulcnsrec  11097  negeq  11413  csbnegg  11418  negsubdi  11478  mulneg1  11614  negfi  12132  deceq1  12654  deceq2  12655  xnegeq  13167  fseq1p1m1  13559  om2uzrdg  13921  uzrdgsuci  13925  seqeq1  13969  seqeq2  13970  seqeq3  13971  seqfeq4  14016  seqof  14024  hashprg  14360  hashtpg  14450  csbwrdg  14509  s1eq  14565  cats1co  14822  s2eqd  14829  s3eqd  14830  s4eqd  14831  s5eqd  14832  s6eqd  14833  s7eqd  14834  s8eqd  14835  xpcogend  14940  shftval  15040  limsupgle  15443  lo1eq  15534  rlimeq  15535  sumeq1  15655  sumeq2w  15658  sumeq2ii  15659  sumeq2sdv  15669  zsum  15684  sumss2  15692  fsumsplitsnun  15721  isumclim3  15725  fsumcom2  15740  incexclem  15802  incexc2  15804  isumshft  15805  prodeq1f  15872  prodeq1  15873  prodeq2w  15876  prodeq2ii  15877  prodeq2sdv  15889  zprod  15903  fprodm1s  15936  fprodp1s  15937  fprodcom2  15950  fprodsplitf  15954  iprodclim3  15966  ef0lem  16044  ruclem7  16204  sadcp1  16425  smupp1  16450  smueqlem  16460  algrp1  16544  dfphi2  16744  prmdiveq  16756  pceulem  16816  vdwlem6  16957  cshwsiun  17070  sloteq  17153  setsid  17177  elbasfv  17185  elbasov  17186  imastset  17485  imasvscaval  17501  isoval  17727  funcoppc  17837  fulloppc  17886  fuccofval  17924  natpropd  17941  catccofval  18066  xpchomfval  18140  xpccofval  18143  lubfval  18309  glbfval  18322  grpidpropd  18589  gsumpropd2lem  18606  frmdplusg  18781  efmndplusg  18807  grpinvpropd  18947  grpsubpropd  18977  grpsubpropd2  18978  mulgpropd  19048  ecqusaddd  19124  oppgmnd  19286  sylow1lem2  19529  sylow3lem1  19557  prds1  20232  pwsmgp  20236  opprrng  20254  rngidpropd  20324  dvdsrpropd  20325  unitpropd  20326  invrpropd  20327  rhm1  20398  rhmopp  20418  rhmsubclem2  20595  lmhmpropd  20980  lidlrsppropd  21154  rngqiprnglinlem2  21202  lpival  21234  pzriprnglem11  21401  zrhpropd  21424  znle  21446  frlmplusgval  21673  frlmvscafval  21675  ressascl  21805  asclpropd  21806  aspval2  21807  psrbas  21842  psrplusg  21845  psrmulr  21851  psrvscafval  21857  resspsrbas  21883  ressmplbas2  21934  opsrle  21954  opsrbaslem  21956  vr1val  22076  ressply1add  22114  ressply1mul  22115  ressply1vsca  22116  psrplusgpropd  22120  mplbaspropd  22121  psropprmul  22122  ply1baspropd  22127  ply1plusgpropd  22128  ply1sca2  22138  ply1ascl0  22139  ply1ascl1  22140  subrgvr1  22147  coe1mul2lem2  22154  ply1coe1eq  22187  evls1addd  22258  evls1muld  22259  evls1vsca  22260  rhmply1vr1  22274  rhmply1vsca  22275  mamudi  22290  mamudir  22291  matrcl  22299  oftpos  22339  mattpos1  22343  mdetfval  22473  mdetrlin  22489  mdetrsca  22490  mdetrsca2  22491  mdetrlin2  22494  mdetunilem5  22503  madufval  22524  madugsum  22530  idmatidpmat  22624  cpmidpmat  22760  cncmp  23279  2ndcsep  23346  llyeq  23357  nllyeq  23358  xkouni  23486  hmphindis  23684  xkocnv  23701  ptcmplem2  23940  snclseqg  24003  prdstmdd  24011  ustexsym  24103  ucnextcn  24191  metreslem  24250  comet  24401  nrmmetd  24462  nmpropd  24482  isngp3  24486  ngpds  24492  subgnm  24521  tngnm  24539  idnghm  24631  cnmetdval  24658  cnmpopc  24822  htpyco2  24878  phtpyco2  24889  clsocv  25150  rrxprds  25289  rrxnm  25291  rrxplusgvscavalb  25295  ovolunlem1a  25397  voliunlem3  25453  ioombl1lem4  25462  uniioombllem4  25487  itg11  25592  itgeq1f  25672  itgeq1fOLD  25673  itgeq1  25674  itgeq2  25679  iblss2  25707  itgss  25713  itgeqa  25715  itgfsum  25728  itgsplit  25737  ditgeq1  25749  ditgeq2  25750  ditgeq3  25751  dvcmulf  25848  dvmptfsum  25879  dvcnvrelem2  25923  mdegfval  25967  mdegpropd  25989  deg1propd  25991  plyeq0  26116  coe11  26158  dgrlt  26172  dgradd2  26174  dgrmulc  26177  dvply1  26191  fta1lem  26215  pserulm  26331  rlimcnp2  26876  jensenlem1  26897  basellem5  26995  dchrbas  27146  dchrrcl  27151  dchrplusg  27158  dchrfi  27166  lgsdi  27245  lgseisenlem2  27287  lgsquadlem3  27293  dchrmusumlema  27404  rpvmasum2  27423  dchrisum0lema  27425  pntlemg  27509  nosupbnd2lem1  27627  lruneq  27818  addsval  27869  mulsval  28012  seqseq123d  28180  colperpexlem2  28658  axlowdimlem13  28881  uhgrvtxedgiedgb  29063  nb3grprlem1  29307  crctcshlem2  29748  wpthswwlks2on  29891  clwlknf1oclwwlkn  30013  frgrncvvdeq  30238  avril1  30392  0vfval  30535  imsval  30614  imsdval  30615  bcseqi  31049  normpythi  31071  cm0  31538  fh1  31547  pjcji  31613  opsqrlem5  32073  pjsdi2i  32086  pjclem3  32126  pjci  32129  golem1  32200  iuneq12daf  32485  iunrdx  32492  ofresid  32566  cnvprop  32619  coprprop  32622  f1od2  32644  dp2eq1  32793  dp2eq2  32794  fzto1st1  33059  gsumvsca1  33179  gsumvsca2  33180  urpropd  33183  resv1r  33311  nsgqusf1olem2  33385  oppr2idl  33457  opprqus0g  33461  ressply1evls1  33534  lindsunlem  33620  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  fldsdrgfldext2  33658  fldextrspunlem1  33670  fldextrspunfld  33671  algextdeglem4  33710  crefeq  33835  rspectopn  33857  xrge0mulc1cn  33931  qqhval2  33972  esumeq12dvaf  34021  esumeq2  34026  esumf1o  34040  esumfzf  34059  esumss  34062  esumpfinvalf  34066  ofceq  34087  carsgclctunlem1  34308  itgeq12dv  34317  ccatmulgnn0dir  34533  breprexpnat  34625  bnj956  34766  bnj1385  34822  bnj96  34855  bnj548  34887  bnj553  34888  bnj554  34889  bnj602  34905  bnj18eq1  34917  bnj1234  35003  bnj1296  35011  bnj1318  35015  bnj1442  35039  bnj1450  35040  cvmliftlem5  35276  cvmliftlem10  35281  cvmlift2lem9  35298  cvmliftphtlem  35304  satfdm  35356  mthmpps  35569  rdgprc  35782  dfrdg2  35783  wsuceq123  35802  wlimeq12  35807  altopthsn  35949  altxpeq1  35961  altxpeq2  35962  ixpeq12dv  36204  prodeq12sdv  36206  itgeq12sdv  36207  ditgeq123dv  36209  cbvcsbdavw  36247  cbvcsbdavw2  36248  cbvrabdavw  36249  cbviundavw  36250  cbviindavw  36251  cbvopab1davw  36252  cbvopab2davw  36253  cbvopabdavw  36254  cbvmptdavw  36255  cbviotadavw  36257  cbvriotadavw  36258  cbvoprab1davw  36259  cbvoprab2davw  36260  cbvoprab3davw  36261  cbvoprab123davw  36262  cbvoprab12davw  36263  cbvoprab23davw  36264  cbvoprab13davw  36265  cbvixpdavw  36266  cbvsumdavw  36267  cbvproddavw  36268  cbvitgdavw  36269  cbvditgdavw  36270  cbvrabdavw2  36273  cbviundavw2  36274  cbviindavw2  36275  cbvmptdavw2  36276  cbvriotadavw2  36278  cbvmpodavw2  36279  cbvmpo1davw2  36280  cbvmpo2davw2  36281  cbvixpdavw2  36282  cbvsumdavw2  36283  cbvproddavw2  36284  cbvitgdavw2  36285  cbvditgdavw2  36286  ee7.2aOLD  36449  bj-sngleq  36955  bj-tageq  36964  bj-projeq  36980  bj-projval  36984  bj-1upleq  36987  bj-pr1eq  36990  bj-pr2eq  37004  bj-evaleq  37060  bj-imafv  37239  csbrecsg  37316  csbrdgg  37317  csboprabg  37318  csbmpo123  37319  finxpeq1  37374  finxpeq2  37375  csbfinxpg  37376  finxpreclem4  37382  cureq  37590  unceq  37591  uncov  37595  unccur  37597  finixpnum  37599  ptrest  37613  poimirlem3  37617  poimirlem9  37623  poimirlem15  37629  poimirlem16  37630  poimirlem26  37640  poimirlem27  37641  mbfposadd  37661  cnambfre  37662  iblabsnclem  37677  ftc1anclem1  37687  heiborlem4  37808  heiborlem6  37810  mpobi123f  38156  iineq12f  38158  mptbi12f  38160  eccnvepres  38268  xrneq1  38363  xrneq2  38366  cosseq  38417  redundss3  38619  riotaclbgBAD  38947  toycom  38966  ldualvbase  39119  ldualfvadd  39121  ldualsca  39125  ldualsbase  39126  ldualsaddN  39127  ldualfvs  39129  ldual0  39140  ldual1  39141  ldualneg  39142  cdleme19f  40302  cdleme20m  40317  cdleme21k  40332  cdleme27b  40362  cdleme31so  40373  cdleme31sn  40374  cdleme31se  40376  cdleme31se2  40377  cdleme31sc  40378  cdleme31sde  40379  cdleme31fv  40384  cdleme40v  40463  cdleme43dN  40486  cdlemeg46ngfr  40512  ltrnco4  40733  tgrpbase  40740  tgrpopr  40741  erngbase  40795  erngfplus  40796  erngfmul  40799  erngbase-rN  40803  erngfplus-rN  40804  erngfmul-rN  40807  dvasca  41000  dvavbase  41007  dvafvadd  41008  dvafvsca  41010  tendocnv  41015  dvhsca  41076  dvhfplusr  41078  dvhvbase  41081  dvhfvadd  41085  dvhfvsca  41094  lcdvadd  41591  lcdsbase  41594  lcdsadd  41595  lcdvs  41597  lcd0  41602  lcd1  41603  lcdneg  41604  fsuppind  42578  imaiinfv  42681  mapfzcons1  42705  rexrabdioph  42782  dnnumch1  43033  dnwech  43037  aomclem6  43048  pwssplit4  43078  pwfi2f1o  43085  mendplusgfval  43170  mendvscafval  43175  harval3  43527  dssmapntrcls  44117  scotteqd  44226  colleq12d  44242  uzmptshftfval  44335  dropab1  44436  dropab2  44437  iineq12dv  45100  rabbida2  45126  rabbida3  45129  itgsinexplem1  45952  wallispi2lem2  46070  fourierdlem36  46141  etransclem4  46236  fcoreslem1  47064  afveq12d  47134  aoveq123d  47179  aovfundmoveq  47182  aovnuoveq  47192  aovvoveq  47193  aovovn0oveq  47195  afv2eq12d  47216  fsumsplitsndif  47374  rngccofvalALTV  48258  rhmsubcALTVlem2  48270  ringccofvalALTV  48292  itscnhlinecirc02plem2  48772  oppfrcl3  49119  oppf1st2nd  49120  uppropd  49170  natoppf  49218  catcrcl  49384  lmdpropd  49646  cmdpropd  49647  lmddu  49656  cmddu  49657  setrecseq  49674  aacllem  49790