Theorem 3eqtr4a 2800

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr4a.1	⊢ 𝐴 = 𝐵
3eqtr4a.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4a.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4a	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr4a

Step	Hyp	Ref	Expression
1		3eqtr4a.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3eqtr4a.1	. . 3 ⊢ 𝐴 = 𝐵
3	1, 2	eqtrdi 2790	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2777	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:  rabsnif  4727  uniintsn  4989  iinvdif  5084  iununi  5103  dmxpid  5943  rnxpid  6194  csbrn  6224  dmsnsnsn  6241  opswap  6250  xpcoid  6311  predres  6361  unizlim  6508  fvco4i  7009  fndmdifcom  7062  fmptsng  7187  fmptsnd  7188  csbov  7475  ordunisuc  7851  offres  8006  1stval2  8029  2ndval2  8030  cnvf1olem  8133  fparlem3  8137  fparlem4  8138  frrlem12  8320  seqomlem1  8488  ecovcom  8861  ecovass  8862  ecovdi  8863  resixpfo  8974  mapunen  9184  cardidm  9996  cardiun  10019  alephcard  10107  cardalephex  10127  cardcf  10289  cfidm  10312  alephsing  10313  itunisuc  10456  itunitc  10458  ituniiun  10459  alephadd  10614  alephreg  10619  pwcfsdom  10620  addcompq  10987  addcomnq  10988  mulcompq  10989  mulcomnq  10990  addassnq  10995  mulassnq  10996  addrid  11438  zeo  12701  xnegneg  13252  xaddcom  13278  xaddrid  13279  xnegdi  13286  xmulrid  13317  xadddilem  13332  ixxin  13400  fzsuc2  13618  expneg  14106  sq01  14260  facp1  14313  bcpasc  14356  hashfzp1  14466  resunimafz0  14480  hashf1lem1  14490  hashf1  14492  ccat1st1st  14662  swrdccatin1  14759  swrdccat3blem  14773  repswsymballbi  14814  cshwmodn  14829  cshwlen  14833  repswcshw  14846  trclun  15049  relexpcnv  15070  relexpaddd  15089  absexp  15339  sqreulem  15394  fsumf1o  15755  fsumadd  15772  fsumrev2  15814  fsumparts  15838  fsumrelem  15839  fprodf1o  15978  fprodmul  15992  fproddiv  15993  fprodfac  16005  fallfacfwd  16068  efexp  16133  tanval2  16165  sadeq  16505  smumullem  16525  smumul  16526  gcdcom  16546  gcd0id  16552  gcdass  16580  nn0expgcd  16597  lcmcom  16626  lcmneg  16636  lcmass  16647  nn0gcdsq  16785  dfphi2  16807  pcneg  16907  setscom  17213  strfvi  17223  fveqprc  17224  oveqprc  17225  setsnidOLD  17243  ressbas  17279  ressbasOLD  17280  ressinbas  17290  ressress  17293  firest  17478  topnval  17480  xpsfeq  17609  xpsaddlem  17619  xpsvsca  17623  oppchomfval  17758  oppchomfvalOLD  17759  oppcbasOLD  17764  rescbas  17876  rescbasOLD  17877  rescco  17880  resccoOLD  17881  cofuass  17939  fucbas  18015  fuchom  18016  fuchomOLD  18017  setccatid  18137  estrccatid  18186  xpcbas  18233  oduleval  18345  odulub  18464  oduglb  18466  ipotset  18590  efmndbas  18896  efmndbasabf  18897  symggrplem  18909  smndex1mndlem  18934  pwmnd  18962  grpinvfvi  19012  cntrval  19349  cntzval  19351  oppgplusfval  19378  snsymgefmndeq  19426  symgvalstruct  19428  symgvalstructOLD  19429  pmtrprfval  19519  m1expaddsub  19530  sylow1lem2  19631  sylow3lem1  19659  oppglsm  19674  gsumzsplit  19959  gsum2dlem2  20003  gsumcom2  20007  dprd2dlem2  20074  dprd2da  20076  dmdprdsplit2lem  20079  mgpplusg  20155  mgpress  20166  mgpressOLD  20167  ringidval  20200  opprmulfval  20352  abvtrivd  20849  sralem  21192  sralemOLD  21193  srasca  21200  srascaOLD  21201  sravsca  21202  sravscaOLD  21203  sraip  21204  rlmval  21215  zlmlemOLD  21545  zlmsca  21552  zlmvsca  21553  psgninv  21617  ocvval  21702  thlbas  21731  thlbasOLD  21732  thlle  21733  thlleOLD  21734  thloc  21736  dsmmval2  21773  psrmulr  21979  mplmonmul  22071  mplcoe3  22073  opsrbaslem  22084  opsrbaslemOLD  22085  opsrtoslem2  22097  psr1val  22202  ply1basfvi  22257  ply1plusgfvi  22258  psr1sca2  22267  evl1fval1lem  22349  mattpos1  22477  mdettpos  22632  smadiadetglem1  22692  tgdif0  23014  indislem  23022  restco  23187  txtopon  23614  txindislem  23656  qtopres  23721  hmphindis  23820  ptuncnv  23830  snclseqg  24139  tsmssplit  24175  ussval  24283  tuslem  24290  tuslemOLD  24291  setsmsbas  24500  setsmsbasOLD  24501  tnglemOLD  24669  tngds  24683  tngdsOLD  24684  tngtset  24685  pcoass  25070  cphsqrtcl2  25233  rrxcph  25439  ovolunlem1a  25544  ioorinv  25624  itg11  25739  itg1mulc  25753  itg2cnlem1  25810  iblss2  25855  ibladdlem  25869  itgfsum  25876  iblabslem  25877  iblabs  25878  ditgneg  25906  deg1fvi  26138  dgrco  26329  logfac  26657  cxpexp  26724  cxpmul2  26745  cxpsqrt  26759  cxpsqrtth  26786  dvcxp1  26796  dvcxp2  26797  ang180lem1  26866  mcubic  26904  quart1  26913  reasinsin  26953  atanlogaddlem  26970  atantayl2  26995  log2tlbnd  27002  basellem2  27139  basellem3  27140  basellem5  27142  basellem8  27145  fsumdvdsmul  27252  dchrmullid  27310  bcp1ctr  27337  lgsneg  27379  lgsneg1  27380  lgsdir2  27388  lgsdir  27390  lgsdi  27392  lgsquad2lem2  27443  pntleml  27669  lrold  27949  abssnid  28281  om2noseqfo  28318  n0seo  28419  zs12bday  28438  motgrp  28565  lmiisolem  28818  ttglemOLD  28900  egrsubgr  29308  iswwlksnon  29882  iswspthsnon  29885  bafval  30632  ipidsq  30738  ipasslem1  30859  pjclem2  32224  cvmdi  32352  imadifxp  32620  2ndimaxp  32662  suppun2  32698  iundisjcnt  32805  dpfrac1  32858  gsumpart  33042  cycpmco2rn  33127  cyc3genpmlem  33153  fracbas  33286  resvsca  33335  rspectset  33826  indval2  33994  bayesth  34420  ofcccat  34536  plymulx  34541  subfacp1lem6  35169  satfdm  35353  mvtval  35484  mexval  35486  mexval2  35487  mdvval  35488  mrsubfval  35492  mrsubvrs  35506  msubfval  35508  elmsubrn  35512  mvhfval  35517  mpstval  35519  msrfval  35521  mstaval  35528  mthmval  35559  bccolsum  35718  dfrdg2  35776  dfrdg3  35777  dfrdg4  35932  ordtoplem  36417  ordcmp  36429  curunc  37588  matunitlindflem2  37603  poimirlem6  37612  poimirlem7  37613  poimirlem11  37617  poimirlem12  37618  poimirlem13  37619  poimirlem14  37620  poimirlem16  37622  poimirlem19  37625  poimirlem21  37627  poimirlem22  37628  poimirlem27  37633  poimirlem31  37637  poimirlem32  37638  itg2addnclem2  37658  ibladdnclem  37662  iblabsnclem  37669  iblabsnc  37670  iblmulc2nc  37671  ftc1anclem8  37686  pmodN  39832  tgrpgrplem  40731  tendoplass  40765  tendoicl  40778  erngdvlem3  40972  dvhvaddass  41079  dib0  41146  dib1dim2  41150  diclspsn  41176  cdlemn8  41186  dihopelvalcpre  41230  djhcom  41387  evlsbagval  42552  kelac2  43053  mendbas  43168  mendring  43176  iscard4  43522  relexp01min  43702  relexpaddss  43707  iotain  44412  addrcom  44470  rnsnf  45126  itgsinexplem1  45909  volioc  45927  dirkertrigeqlem1  46053  fourierdlem104  46165  sqwvfoura  46183  sqwvfourb  46184  fzopredsuc  47272  fppr2odd  47655  dfnbgr5  47774  rngccatidALTV  48115  ringccatidALTV  48149  0dig2pr01  48459  nn0sumshdiglemB  48469