Theorem 3eqtr4a 2670

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

Syntax hints:   → wi 4   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  rabsnif  4202  uniintsn  4449  iinvdif  4528  iununi  4546  dmxpid  5266  rnxpid  5486  csbrn  5514  dmsnsnsn  5531  opswap  5540  xpcoid  5593  unizlim  5761  fvco4i  6186  fndmdifcom  6230  fmptsng  6339  fmptsnd  6340  csbov  6586  ordunisuc  6924  offres  7054  1stval2  7076  2ndval2  7077  cnvf1olem  7162  fparlem3  7166  fparlem4  7167  imacosupp  7222  seqomlem1  7432  ecovcom  7741  ecovass  7742  ecovdi  7743  resixpfo  7832  mapunen  8014  cardidm  8668  cardiun  8691  alephcard  8776  cardalephex  8796  cardcf  8957  cfidm  8980  alephsing  8981  itunisuc  9124  itunitc  9126  ituniiun  9127  alephadd  9278  alephreg  9283  pwcfsdom  9284  addcompq  9651  addcomnq  9652  mulcompq  9653  mulcomnq  9654  addassnq  9659  mulassnq  9660  addid1  10095  zeo  11339  xnegneg  11919  xaddcom  11945  xaddid1  11946  xnegdi  11950  xmulid1  11981  xadddilem  11996  ixxin  12063  fzsuc2  12268  expneg  12730  sq01  12848  facp1  12927  bcpasc  12970  hashfzp1  13078  hashf1lem1  13096  hashf1  13098  swrdccatin1  13334  swrdccat3blem  13346  repswsymballbi  13378  cshwmodn  13392  repswcshw  13409  trclun  13603  relexpcnv  13623  absexp  13892  sqreulem  13947  fsumf1o  14301  fsumadd  14317  fsumrev2  14356  fsumparts  14379  fsumrelem  14380  pwm1geoser  14439  fprodf1o  14515  fprodmul  14529  fproddiv  14530  fprodfac  14542  fallfacfwd  14606  efexp  14670  tanval2  14702  sqr2irrlem  14816  sadeq  15032  smumullem  15052  smumul  15053  gcdcom  15073  gcd0id  15078  gcdass  15102  lcmcom  15144  lcmneg  15154  lcmass  15165  nn0gcdsq  15298  dfphi2  15317  pcneg  15416  setscom  15731  strfvi  15741  setsnid  15743  ressbas  15757  ressinbas  15763  ressress  15765  firest  15916  topnval  15918  xpsfeq  16047  xpsaddlem  16058  xpsvsca  16062  homffval  16173  oppchomfval  16197  oppcbas  16201  rescbas  16312  rescco  16315  cofuass  16372  fucbas  16443  fuchom  16444  setccatid  16557  estrccatid  16595  xpcbas  16641  xpchomfval  16642  xpccofval  16645  oduleval  16954  oduglb  16962  odulub  16964  ipotset  16980  grpinvfvi  17286  cntrval  17575  cntzval  17577  oppgplusfval  17601  symgbas  17623  symggrp  17643  pmtrprfval  17730  m1expaddsub  17741  sylow1lem2  17837  sylow3lem1  17865  oppglsm  17880  gsumzsplit  18150  gsum2dlem2  18193  gsumcom2  18197  dprd2dlem2  18262  dprd2da  18264  dmdprdsplit2lem  18267  mgpplusg  18316  mgpress  18323  ringidval  18326  opprmulfval  18448  abvtrivd  18663  sralem  18998  srasca  19002  sravsca  19003  sraip  19004  rlmval  19012  psrmulr  19205  mplmonmul  19285  mplcoe3  19287  opsrbaslem  19298  opsrbaslemOLD  19299  opsrtoslem2  19306  psr1val  19377  ply1basfvi  19432  ply1plusgfvi  19433  psr1sca2  19442  evl1fval1lem  19515  zlmlem  19684  zlmsca  19688  zlmvsca  19689  psgninv  19747  ocvval  19830  thlbas  19859  thlle  19860  thloc  19862  dsmmval2  19899  mattpos1  20081  mdettpos  20236  smadiadetglem1  20296  tgdif0  20607  indislem  20614  restco  20778  txtopon  21204  txindislem  21246  qtopres  21311  hmphindis  21410  ptuncnv  21420  snclseqg  21729  tsmssplit  21765  ussval  21873  tuslem  21881  setsmsbas  22090  tnglem  22254  tngds  22262  tngtset  22263  pcoass  22632  cphsqrtcl2  22794  rrxcph  22988  ovolunlem1a  23071  ioorinv  23150  itg11  23264  itg1mulc  23277  itg2cnlem1  23334  iblss2  23378  ibladdlem  23392  itgfsum  23399  iblabslem  23400  iblabs  23401  ditgneg  23427  deg1fvi  23649  dgrco  23835  logfac  24151  cxpexp  24214  cxpmul2  24235  cxpsqrt  24249  dvcxp1  24281  dvcxp2  24282  ang180lem1  24339  mcubic  24374  quart1  24383  reasinsin  24423  atanlogaddlem  24440  atantayl2  24465  log2tlbnd  24472  basellem2  24608  basellem3  24609  basellem5  24611  basellem8  24614  dchrmulid2  24777  bcp1ctr  24804  lgsneg  24846  lgsneg1  24847  lgsdir2  24855  lgsdir  24857  lgsdi  24859  lgsquad2lem2  24910  pntleml  25100  motgrp  25238  lmiisolem  25488  ttglem  25556  uhgrstrrepe  25745  eupath2lem3  26506  bafval  26843  ipidsq  26949  ipasslem1  27070  pjclem2  28439  cvmdi  28567  imadifxp  28796  iundisjcnt  28944  resvsca  29161  indval2  29404  bayesth  29828  plymulx  29951  subfacp1lem6  30421  mvtval  30651  mexval  30653  mexval2  30654  mdvval  30655  mrsubfval  30659  mrsubvrs  30673  msubfval  30675  elmsubrn  30679  mvhfval  30684  mpstval  30686  msrfval  30688  mstaval  30695  mthmval  30726  bccolsum  30878  dfrdg2  30945  dfrdg3  30946  dfrdg4  31228  ordtoplem  31604  ordcmp  31616  curunc  32561  matunitlindflem2  32576  poimirlem6  32585  poimirlem7  32586  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem14  32593  poimirlem16  32595  poimirlem19  32598  poimirlem21  32600  poimirlem22  32601  poimirlem27  32606  poimirlem31  32610  poimirlem32  32611  itg2addnclem2  32632  ibladdnclem  32636  iblabsnclem  32643  iblabsnc  32644  iblmulc2nc  32645  ftc1anclem8  32662  pmodN  34154  tgrpgrplem  35055  tendoplass  35089  tendoicl  35102  erngdvlem3  35296  dvhvaddass  35404  dib0  35471  dib1dim2  35475  diclspsn  35501  cdlemn8  35511  dihopelvalcpre  35555  djhcom  35712  kelac2  36653  mendbas  36773  mendsca  36778  mendring  36781  relexp01min  37024  relexpaddss  37029  iotain  37640  addrcom  37700  itgsinexplem1  38845  volioc  38864  dirkertrigeqlem1  38991  fourierdlem104  39103  sqwvfoura  39121  sqwvfourb  39122  fzopredsuc  39946  opidg  40316  resunimafz0  40368  egrsubgr  40501  iswwlksnon  41051  iswspthsnon  41052  rngccatidALTV  41781  ringccatidALTV  41844  0dig2pr01  42202  nn0sumshdiglemB  42212  dpfrac1  42312  dpfrac1OLD  42313