Theorem 3eqtr4a 2823

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

Syntax hints:   → wi 4   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  rabsnif  4682  uniintsn  4943  iinvdif  5037  iununi  5056  csbcnv  5858  dmxpid  5906  rnxpid  6159  csbrn  6190  dmsnsnsn  6207  opswap  6216  xpcoid  6277  predres  6326  unizlim  6470  fvco4i  6969  fndmdifcom  7024  fmptsng  7152  fmptsnd  7153  csbov  7441  ordunisuc  7812  offres  7964  1stval2  7987  2ndval2  7988  cnvf1olem  8089  fparlem3  8093  fparlem4  8094  frrlem12  8278  seqomlem1  8421  ecovcom  8805  ecovass  8806  ecovdi  8807  resixpfo  8918  mapunen  9118  cardidm  9917  cardiun  9940  alephcard  10026  cardalephex  10046  cardcf  10208  cfidm  10232  alephsing  10233  itunisuc  10376  itunitc  10378  ituniiun  10379  alephadd  10535  alephreg  10540  pwcfsdom  10541  addcompq  10908  addcomnq  10909  mulcompq  10910  mulcomnq  10911  addassnq  10916  mulassnq  10917  addrid  11363  indval2  12200  zeo  12659  xnegneg  13217  xaddcom  13243  xaddrid  13244  xnegdi  13251  xmulrid  13282  xadddilem  13297  ixxin  13366  fzsuc2  13587  expneg  14082  sq01  14238  facp1  14291  bcpasc  14334  hashfzp1  14444  resunimafz0  14458  hashf1lem1  14468  hashf1  14470  ccat1st1st  14642  swrdccatin1  14738  swrdccat3blem  14752  repswsymballbi  14793  cshwmodn  14808  cshwlen  14812  repswcshw  14825  trclun  15027  relexpcnv  15048  relexpaddd  15067  absexp  15331  sqreulem  15387  fsumf1o  15750  fsumadd  15767  fsumrev2  15809  fsumparts  15834  fsumrelem  15835  fprodf1o  15976  fprodmul  15990  fproddiv  15991  fprodfac  16003  fallfacfwd  16066  efexp  16133  tanval2  16165  sadeq  16506  smumullem  16526  smumul  16527  gcdcom  16547  gcd0id  16553  gcdass  16581  nn0expgcd  16598  lcmcom  16627  lcmneg  16637  lcmass  16648  nn0gcdsq  16787  dfphi2  16809  pcneg  16910  setscom  17216  strfvi  17226  fveqprc  17227  oveqprc  17228  ressbas  17272  ressinbas  17281  ressress  17283  firest  17461  topnval  17463  xpsfeq  17593  xpsaddlem  17603  xpsvsca  17607  oppchomfval  17746  rescbas  17862  rescco  17865  cofuass  17922  fucbas  17996  fuchom  17997  setccatid  18117  estrccatid  18164  xpcbas  18210  oduleval  18321  odulub  18437  oduglb  18439  ipotset  18565  efmndbas  18905  efmndbasabf  18906  symggrplem  18918  smndex1mndlem  18946  pwmnd  18974  grpinvfvi  19024  cntrval  19359  cntzval  19361  oppgplusfval  19388  snsymgefmndeq  19435  symgvalstruct  19437  pmtrprfval  19527  m1expaddsub  19538  sylow1lem2  19639  sylow3lem1  19667  oppglsm  19682  gsumzsplit  19967  gsum2dlem2  20011  gsumcom2  20015  dprd2dlem2  20082  dprd2da  20084  dmdprdsplit2lem  20087  mgpplusg  20190  mgpress  20196  ringidval  20229  opprmulfval  20384  abvtrivd  20878  sralem  21240  srasca  21244  sravsca  21245  sraip  21246  rlmval  21255  zlmsca  21569  zlmvsca  21570  psgninv  21631  ocvval  21716  thlbas  21745  thlle  21746  thloc  21748  dsmmval2  21785  psrmulr  21991  mplmonmul  22086  mplcoe3  22088  opsrbaslem  22099  opsrtoslem2  22106  psr1val  22245  ply1basfvi  22299  ply1plusgfvi  22300  psr1sca2  22309  evl1fval1lem  22390  mattpos1  22513  mdettpos  22668  smadiadetglem1  22728  tgdif0  23049  indislem  23057  restco  23221  txtopon  23648  txindislem  23690  qtopres  23755  hmphindis  23854  ptuncnv  23864  snclseqg  24173  tsmssplit  24209  ussval  24316  tuslem  24323  setsmsbas  24532  tngds  24705  tngtset  24706  pcoass  25083  cphsqrtcl2  25245  rrxcph  25451  ovolunlem1a  25555  ioorinv  25635  itg11  25750  itg1mulc  25763  itg2cnlem1  25820  iblss2  25865  ibladdlem  25879  itgfsum  25886  iblabslem  25887  iblabs  25888  ditgneg  25916  deg1fvi  26142  dgrco  26332  plymulidp  26343  logfac  26663  cxpexp  26730  cxpmul2  26751  cxpsqrt  26765  cxpsqrtth  26792  dvcxp1  26802  dvcxp2  26803  ang180lem1  26871  mcubic  26909  quart1  26918  reasinsin  26958  atanlogaddlem  26975  atantayl2  27000  log2tlbnd  27007  basellem2  27143  basellem3  27144  basellem5  27146  basellem8  27149  fsumdvdsmul  27256  dchrmullid  27313  bcp1ctr  27340  lgsneg  27382  lgsneg1  27383  lgsdir2  27391  lgsdir  27393  lgsdi  27395  lgsquad2lem2  27446  pntleml  27672  lrold  27987  abssnid  28333  om2noseqfo  28388  n0seo  28511  pw2cutp1  28551  motgrp  28709  lmiisolem  28966  egrsubgr  29475  iswwlksnon  30050  iswspthsnon  30053  bafval  30804  ipidsq  30910  ipasslem1  31031  pjclem2  32396  cvmdi  32524  imadifxp  32798  2ndimaxp  32845  suppun2  32883  iundisjcnt  32997  dpfrac1  33066  gsumpart  33240  suppgsumssiun  33249  cycpmco2rn  33302  cyc3genpmlem  33328  fracbas  33489  resvsca  33515  psrgsum  33842  psrmonmul  33844  psrmonprod  33846  rspectset  34160  bayesth  34733  ofcccat  34837  subfacp1lem6  35532  satfdm  35716  mvtval  35847  mexval  35849  mexval2  35850  mdvval  35851  mrsubfval  35855  mrsubvrs  35869  msubfval  35871  elmsubrn  35875  mvhfval  35880  mpstval  35882  msrfval  35884  mstaval  35891  mthmval  35922  bccolsum  36086  dfrdg2  36140  dfrdg3  36141  dfrdg4  36298  ordtoplem  36792  ordcmp  36804  curunc  38098  matunitlindflem2  38113  poimirlem6  38122  poimirlem7  38123  poimirlem11  38127  poimirlem12  38128  poimirlem13  38129  poimirlem14  38130  poimirlem16  38132  poimirlem19  38135  poimirlem21  38137  poimirlem22  38138  poimirlem27  38143  poimirlem31  38147  poimirlem32  38148  itg2addnclem2  38168  ibladdnclem  38172  iblabsnclem  38179  iblabsnc  38180  iblmulc2nc  38181  ftc1anclem8  38196  pmodN  40471  tgrpgrplem  41370  tendoplass  41404  tendoicl  41417  erngdvlem3  41611  dvhvaddass  41718  dib0  41785  dib1dim2  41789  diclspsn  41815  cdlemn8  41825  dihopelvalcpre  41869  djhcom  42026  evlsbagval  43165  kelac2  43639  mendbas  43754  mendring  43762  iscard4  44106  relexp01min  44286  relexpaddss  44291  iotain  44990  addrcom  45047  rnsnf  45759  limsupvaluz  46279  itgsinexplem1  46525  volioc  46543  dirkertrigeqlem1  46669  fourierdlem104  46781  sqwvfoura  46799  sqwvfourb  46800  hoicvr  47119  fzopredsuc  47915  ppivalnn  48238  fppr2odd  48350  dfnbgr5  48470  gpgprismgr4cycllem10  48723  rngccatidALTV  48891  ringccatidALTV  48925  0dig2pr01  49229  nn0sumshdiglemB  49239  imaidfu2  49729  oppczeroo  49855  dfswapf2  49879  oppc1stf  49906  oppc2ndf  49907  prcof1  50006  setc1onsubc  50220  termolmd  50288