Theorem 3eqtr4a 2834

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

Syntax hints:   → wi 4   = wceq 1507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-9 2057  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765

This theorem is referenced by:  rabsnif  4527  uniintsn  4780  iinvdif  4862  iununi  4881  dmxpid  5636  rnxpid  5864  csbrn  5893  dmsnsnsn  5910  opswap  5919  xpcoid  5973  unizlim  6139  fvco4i  6583  fndmdifcom  6632  fmptsng  6747  fmptsnd  6748  csbov  7012  ordunisuc  7357  offres  7489  1stval2  7511  2ndval2  7512  cnvf1olem  7606  fparlem3  7610  fparlem4  7611  imacosuppOLD  7671  seqomlem1  7882  ecovcom  8195  ecovass  8196  ecovdi  8197  resixpfo  8289  mapunen  8474  cardidm  9174  cardiun  9197  alephcard  9282  cardalephex  9302  cardcf  9464  cfidm  9487  alephsing  9488  itunisuc  9631  itunitc  9633  ituniiun  9634  alephadd  9789  alephreg  9794  pwcfsdom  9795  addcompq  10162  addcomnq  10163  mulcompq  10164  mulcomnq  10165  addassnq  10170  mulassnq  10171  addid1  10612  zeo  11874  xnegneg  12417  xaddcom  12443  xaddid1  12444  xnegdi  12450  xmulid1  12481  xadddilem  12496  ixxin  12564  fzsuc2  12774  expneg  13245  sq01  13394  facp1  13446  bcpasc  13489  hashfzp1  13595  resunimafz0  13606  hashf1lem1  13616  hashf1  13618  ccat1st1st  13781  swrdccatin1  13914  swrdccat3blem  13934  repswsymballbi  13989  cshwmodn  14009  repswcshw  14026  trclun  14225  relexpcnv  14245  absexp  14515  sqreulem  14570  fsumf1o  14930  fsumadd  14946  fsumrev2  14987  fsumparts  15011  fsumrelem  15012  pwm1geoserOLD  15075  fprodf1o  15150  fprodmul  15164  fproddiv  15165  fprodfac  15177  fallfacfwd  15240  efexp  15304  tanval2  15336  sadeq  15671  smumullem  15691  smumul  15692  gcdcom  15712  gcd0id  15717  gcdass  15741  lcmcom  15783  lcmneg  15793  lcmass  15804  nn0gcdsq  15938  dfphi2  15957  pcneg  16056  setscom  16373  strfvi  16383  setsnid  16385  ressbas  16400  ressinbas  16406  ressress  16408  firest  16552  topnval  16554  xpsfeq  16683  xpsaddlem  16694  xpsvsca  16698  homffval  16808  oppchomfval  16832  oppcbas  16836  rescbas  16947  rescco  16950  cofuass  17007  fucbas  17078  fuchom  17079  setccatid  17192  estrccatid  17230  xpcbas  17276  xpchomfval  17277  xpccofval  17280  oduleval  17589  oduglb  17597  odulub  17599  ipotset  17615  grpinvfvi  17923  cntrval  18210  cntzval  18212  oppgplusfval  18237  symgbas  18259  symggrp  18279  pmtrprfval  18366  m1expaddsub  18378  sylow1lem2  18475  sylow3lem1  18503  oppglsm  18518  gsumzsplit  18790  gsum2dlem2  18834  gsumcom2  18838  dprd2dlem2  18902  dprd2da  18904  dmdprdsplit2lem  18907  mgpplusg  18956  mgpress  18963  ringidval  18966  opprmulfval  19088  abvtrivd  19323  sralem  19661  srasca  19665  sravsca  19666  sraip  19667  rlmval  19675  psrmulr  19868  mplmonmul  19948  mplcoe3  19950  opsrbaslem  19961  opsrtoslem2  19968  psr1val  20047  ply1basfvi  20102  ply1plusgfvi  20103  psr1sca2  20112  evl1fval1lem  20185  zlmlem  20356  zlmsca  20360  zlmvsca  20361  psgninv  20418  ocvval  20503  thlbas  20532  thlle  20533  thloc  20535  dsmmval2  20572  mattpos1  20759  mdettpos  20914  smadiadetglem1  20974  tgdif0  21294  indislem  21302  restco  21466  txtopon  21893  txindislem  21935  qtopres  22000  hmphindis  22099  ptuncnv  22109  snclseqg  22417  tsmssplit  22453  ussval  22561  tuslem  22569  setsmsbas  22778  tnglem  22942  tngds  22950  tngtset  22951  pcoass  23321  cphsqrtcl2  23483  rrxcph  23688  ovolunlem1a  23790  ioorinv  23870  itg11  23985  itg1mulc  23998  itg2cnlem1  24055  iblss2  24099  ibladdlem  24113  itgfsum  24120  iblabslem  24121  iblabs  24122  ditgneg  24148  deg1fvi  24372  dgrco  24558  logfac  24875  cxpexp  24942  cxpmul2  24963  cxpsqrt  24977  cxpsqrtth  25003  dvcxp1  25012  dvcxp2  25013  ang180lem1  25078  mcubic  25116  quart1  25125  reasinsin  25165  atanlogaddlem  25182  atantayl2  25207  log2tlbnd  25215  basellem2  25351  basellem3  25352  basellem5  25354  basellem8  25357  dchrmulid2  25520  bcp1ctr  25547  lgsneg  25589  lgsneg1  25590  lgsdir2  25598  lgsdir  25600  lgsdi  25602  lgsquad2lem2  25653  pntleml  25879  motgrp  26021  lmiisolem  26274  ttglem  26355  egrsubgr  26752  iswwlksnon  27329  iswspthsnon  27332  bafval  28148  ipidsq  28254  ipasslem1  28375  pjclem2  29744  cvmdi  29872  imadifxp  30107  iundisjcnt  30259  dpfrac1  30303  resvsca  30538  indval2  30874  bayesth  31300  plymulx  31425  subfacp1lem6  31977  mvtval  32207  mexval  32209  mexval2  32210  mdvval  32211  mrsubfval  32215  mrsubvrs  32229  msubfval  32231  elmsubrn  32235  mvhfval  32240  mpstval  32242  msrfval  32244  mstaval  32251  mthmval  32282  bccolsum  32431  dfrdg2  32501  dfrdg3  32502  frrlem12  32595  dfrdg4  32873  ordtoplem  33243  ordcmp  33255  curunc  34263  matunitlindflem2  34278  poimirlem6  34287  poimirlem7  34288  poimirlem11  34292  poimirlem12  34293  poimirlem13  34294  poimirlem14  34295  poimirlem16  34297  poimirlem19  34300  poimirlem21  34302  poimirlem22  34303  poimirlem27  34308  poimirlem31  34312  poimirlem32  34313  itg2addnclem2  34333  ibladdnclem  34337  iblabsnclem  34344  iblabsnc  34345  iblmulc2nc  34346  ftc1anclem8  34363  pmodN  36379  tgrpgrplem  37278  tendoplass  37312  tendoicl  37325  erngdvlem3  37519  dvhvaddass  37626  dib0  37693  dib1dim2  37697  diclspsn  37723  cdlemn8  37733  dihopelvalcpre  37777  djhcom  37934  nn0expgcd  38561  kelac2  39006  mendbas  39125  mendsca  39130  mendring  39133  relexp01min  39366  relexpaddss  39371  iotain  40110  addrcom  40170  rnsnf  40814  itgsinexplem1  41615  volioc  41633  dirkertrigeqlem1  41760  fourierdlem104  41872  sqwvfoura  41890  sqwvfourb  41891  fzopredsuc  42875  fppr2odd  43204  rngccatidALTV  43564  ringccatidALTV  43627  0dig2pr01  43978  nn0sumshdiglemB  43988