Theorem 3eqtr4a 2826

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 2816	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2803	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 2156  ax-ext 2737

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

This theorem is used by:  rabsnif  4691  uniintsn  4952  iinvdif  5048  iununi  5067  csbcnv  5874  dmxpid  5922  rnxpid  6173  csbrn  6206  dmsnsnsn  6223  opswap  6232  xpcoid  6295  predres  6344  unizlim  6489  fvco4i  6987  fndmdifcom  7042  fmptsng  7172  fmptsnd  7173  csbov  7464  ordunisuc  7834  offres  7986  1stval2  8009  2ndval2  8010  cnvf1olem  8111  fparlem3  8115  fparlem4  8116  frrlem12  8300  seqomlem1  8443  ecovcom  8827  ecovass  8828  ecovdi  8829  resixpfo  8940  mapunen  9141  cardidm  9961  cardiun  9984  alephcard  10070  cardalephex  10090  cardcf  10250  cfidm  10274  alephsing  10275  itunisuc  10418  itunitc  10420  ituniiun  10421  alephadd  10577  alephreg  10582  pwcfsdom  10583  addcompq  10950  addcomnq  10951  mulcompq  10952  mulcomnq  10953  addassnq  10958  mulassnq  10959  addrid  11405  indval2  12238  zeo  12698  xnegneg  13256  xaddcom  13282  xaddrid  13283  xnegdi  13290  xmulrid  13321  xadddilem  13336  ixxin  13405  fzsuc2  13627  expneg  14123  sq01  14279  facp1  14332  bcpasc  14375  hashfzp1  14486  resunimafz0  14500  hashf1lem1  14510  hashf1  14512  ccat1st1st  14686  swrdccatin1  14784  swrdccat3blem  14798  repswsymballbi  14841  cshwmodn  14856  cshwlen  14860  repswcshw  14873  trclun  15075  relexpcnv  15096  relexpaddd  15115  absexp  15379  sqreulem  15435  fsumf1o  15797  fsumadd  15814  fsumrev2  15856  fsumparts  15881  fsumrelem  15882  fprodf1o  16023  fprodmul  16037  fproddiv  16038  fprodfac  16050  fallfacfwd  16112  efexp  16179  tanval2  16211  sadeq  16552  smumullem  16572  smumul  16573  gcdcom  16593  gcd0id  16599  gcdass  16627  nn0expgcd  16644  lcmcom  16673  lcmneg  16683  lcmass  16694  nn0gcdsq  16833  dfphi2  16855  pcneg  16956  setscom  17262  strfvi  17272  fveqprc  17273  oveqprc  17274  ressbas  17318  ressinbas  17327  ressress  17329  firest  17507  topnval  17509  xpsfeq  17639  xpsaddlem  17649  xpsvsca  17653  oppchomfval  17792  rescbas  17908  rescco  17911  cofuass  17968  fucbas  18042  fuchom  18043  setccatid  18163  estrccatid  18210  xpcbas  18256  oduleval  18367  odulub  18483  oduglb  18485  ipotset  18611  mgmn0plusgplusf  18732  efmndbas  18967  efmndbasabf  18968  symggrplem  18980  smndex1mndlem  19008  pwmnd  19043  grpinvfvi  19093  cntrval  19433  cntzval  19435  oppgplusfval  19462  snsymgefmndeq  19509  symgvalstruct  19511  pmtrprfval  19601  m1expaddsub  19612  sylow1lem2  19713  sylow3lem1  19741  oppglsm  19756  gsumzsplit  20041  gsum2dlem2  20085  gsumcom2  20089  dprd2dlem2  20156  dprd2da  20158  dmdprdsplit2lem  20161  mgpplusg  20264  mgpress  20270  ringidval  20309  opprmulfval  20467  abvtrivd  20985  sralem  21347  srasca  21351  sravsca  21352  sraip  21353  rlmval  21362  zlmsca  21720  zlmvsca  21721  psgninv  21782  ocvval  21867  thlbas  21896  thlle  21897  thloc  21899  dsmmval2  21936  psrmulr  22142  mplmonmul  22237  mplcoe3  22239  opsrbaslem  22250  opsrtoslem2  22257  psr1val  22396  ply1basfvi  22450  ply1plusgfvi  22451  psr1sca2  22460  evl1fval1lem  22540  mattpos1  22663  mdettpos  22818  smadiadetglem1  22878  tgdif0  23199  indislem  23207  restco  23371  txtopon  23799  txindislem  23841  qtopres  23906  hmphindis  24005  ptuncnv  24015  snclseqg  24324  tsmssplit  24360  ussval  24467  tuslem  24474  setsmsbas  24683  tngds  24856  tngtset  24857  pcoass  25234  cphsqrtcl2  25396  rrxcph  25602  ovolunlem1a  25706  ioorinv  25786  itg11  25901  itg1mulc  25914  itg2cnlem1  25971  iblss2  26016  ibladdlem  26030  itgfsum  26037  iblabslem  26038  iblabs  26039  ditgneg  26067  deg1fvi  26293  dgrco  26483  plymulidp  26494  logfac  26817  cxpexp  26884  cxpmul2  26905  cxpsqrt  26919  cxpsqrtth  26946  dvcxp1  26956  dvcxp2  26957  ang180lem1  27025  mcubic  27063  quart1  27072  reasinsin  27112  atanlogaddlem  27129  atantayl2  27154  log2tlbnd  27161  basellem2  27297  basellem3  27298  basellem5  27300  basellem8  27303  fsumdvdsmul  27410  dchrmullid  27467  bcp1ctr  27494  lgsneg  27536  lgsneg1  27537  lgsdir2  27545  lgsdir  27547  lgsdi  27549  lgsquad2lem2  27600  pntleml  27826  lrold  28141  abssnid  28487  om2noseqfo  28542  n0seo  28665  pw2cutp1  28705  motgrp  28863  lmiisolem  29156  egrsubgr  29685  iswwlksnon  30269  iswspthsnon  30272  bafval  31027  ipidsq  31133  ipasslem1  31254  pjclem2  32619  cvmdi  32747  imadifxp  33017  2ndimaxp  33062  suppun2  33100  iundisjcnt  33213  dpfrac1  33281  gsumpart  33447  suppgsumssiun  33456  cycpmco2rn  33509  cyc3genpmlem  33535  fracbas  33690  resvsca  33716  psrgsum  34002  psrmonmul  34004  psrmonprod  34006  rspectset  34320  bayesth  34894  ofcccat  34998  subfacp1lem6  35714  satfdm  35898  mvtval  36029  mexval  36031  mexval2  36032  mdvval  36033  mrsubfval  36037  mrsubvrs  36051  msubfval  36053  elmsubrn  36057  mvhfval  36062  mpstval  36064  msrfval  36066  mstaval  36073  mthmval  36104  bccolsum  36268  dfrdg2  36322  dfrdg3  36323  dfrdg4  36480  ordtoplem  37003  ordcmp  37015  curunc  38310  matunitlindflem2  38325  poimirlem6  38334  poimirlem7  38335  poimirlem11  38339  poimirlem12  38340  poimirlem13  38341  poimirlem14  38342  poimirlem16  38344  poimirlem19  38347  poimirlem21  38349  poimirlem22  38350  poimirlem27  38355  poimirlem31  38359  poimirlem32  38360  itg2addnclem2  38380  ibladdnclem  38384  iblabsnclem  38391  iblabsnc  38392  iblmulc2nc  38393  ftc1anclem8  38408  pmodN  40682  tgrpgrplem  41581  tendoplass  41615  tendoicl  41628  erngdvlem3  41822  dvhvaddass  41929  dib0  41996  dib1dim2  42000  diclspsn  42026  cdlemn8  42036  dihopelvalcpre  42080  djhcom  42237  evlsbagval  43376  kelac2  43850  mendbas  43965  mendring  43973  iscard4  44317  relexp01min  44497  relexpaddss  44502  iotain  45185  addrcom  45241  rnsnf  45960  limsupvaluz  46480  itgsinexplem1  46726  volioc  46744  dirkertrigeqlem1  46870  fourierdlem104  46982  sqwvfoura  47000  sqwvfourb  47001  hoicvr  47320  fzopredsuc  48119  ppivalnn  48442  fppr2odd  48554  dfnbgr5  48674  gpgprismgr4cycllem10  48927  rngccatidALTV  49094  ringccatidALTV  49128  0dig2pr01  49447  nn0sumshdiglemB  49457  imaidfu2  49946  oppczeroo  50072  dfswapf2  50096  oppc1stf  50123  oppc2ndf  50124  prcof1  50223  setc1onsubc  50437  termolmd  50505