Theorem 3eqtr4a 2805

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731

This theorem is referenced by:  rabsnif  4664  uniintsn  4923  iinvdif  5013  iununi  5032  dmxpid  5836  rnxpid  6073  csbrn  6103  dmsnsnsn  6120  opswap  6129  xpcoid  6190  predres  6239  unizlim  6380  fvco4i  6863  fndmdifcom  6914  fmptsng  7034  fmptsnd  7035  csbov  7311  ordunisuc  7667  offres  7812  1stval2  7834  2ndval2  7835  cnvf1olem  7934  fparlem3  7938  fparlem4  7939  frrlem12  8097  seqomlem1  8265  ecovcom  8586  ecovass  8587  ecovdi  8588  resixpfo  8698  mapunen  8898  cardidm  9701  cardiun  9724  alephcard  9810  cardalephex  9830  cardcf  9992  cfidm  10015  alephsing  10016  itunisuc  10159  itunitc  10161  ituniiun  10162  alephadd  10317  alephreg  10322  pwcfsdom  10323  addcompq  10690  addcomnq  10691  mulcompq  10692  mulcomnq  10693  addassnq  10698  mulassnq  10699  addid1  11138  zeo  12389  xnegneg  12930  xaddcom  12956  xaddid1  12957  xnegdi  12964  xmulid1  12995  xadddilem  13010  ixxin  13078  fzsuc2  13296  expneg  13771  sq01  13921  facp1  13973  bcpasc  14016  hashfzp1  14127  resunimafz0  14138  hashf1lem1  14149  hashf1lem1OLD  14150  hashf1  14152  ccat1st1st  14316  swrdccatin1  14419  swrdccat3blem  14433  repswsymballbi  14474  cshwmodn  14489  cshwlen  14493  repswcshw  14506  trclun  14706  relexpcnv  14727  relexpaddd  14746  absexp  14997  sqreulem  15052  fsumf1o  15416  fsumadd  15433  fsumrev2  15475  fsumparts  15499  fsumrelem  15500  fprodf1o  15637  fprodmul  15651  fproddiv  15652  fprodfac  15664  fallfacfwd  15727  efexp  15791  tanval2  15823  sadeq  16160  smumullem  16180  smumul  16181  gcdcom  16201  gcd0id  16207  gcdass  16236  lcmcom  16279  lcmneg  16289  lcmass  16300  nn0gcdsq  16437  dfphi2  16456  pcneg  16556  setscom  16862  strfvi  16872  fveqprc  16873  oveqprc  16874  setsnidOLD  16892  ressbas  16928  ressbasOLD  16929  ressinbas  16936  ressress  16939  firest  17124  topnval  17126  xpsfeq  17255  xpsaddlem  17265  xpsvsca  17269  oppchomfval  17404  oppchomfvalOLD  17405  oppcbasOLD  17410  rescbas  17522  rescbasOLD  17523  rescco  17526  resccoOLD  17527  cofuass  17585  fucbas  17658  fuchom  17659  fuchomOLD  17660  setccatid  17780  estrccatid  17829  xpcbas  17876  oduleval  17988  odulub  18106  oduglb  18108  ipotset  18232  efmndbas  18491  efmndbasabf  18492  symggrplem  18504  smndex1mndlem  18529  pwmnd  18557  grpinvfvi  18603  cntrval  18906  cntzval  18908  oppgplusfval  18933  snsymgefmndeq  18983  symgvalstruct  18985  symgvalstructOLD  18986  pmtrprfval  19076  m1expaddsub  19087  sylow1lem2  19185  sylow3lem1  19213  oppglsm  19228  gsumzsplit  19509  gsum2dlem2  19553  gsumcom2  19557  dprd2dlem2  19624  dprd2da  19626  dmdprdsplit2lem  19629  mgpplusg  19705  mgpress  19716  mgpressOLD  19717  ringidval  19720  opprmulfval  19845  abvtrivd  20081  sralem  20420  sralemOLD  20421  srasca  20428  srascaOLD  20429  sravsca  20430  sravscaOLD  20431  sraip  20432  rlmval  20442  zlmlemOLD  20700  zlmsca  20707  zlmvsca  20708  psgninv  20768  ocvval  20853  thlbas  20882  thlbasOLD  20883  thlle  20884  thlleOLD  20885  thloc  20887  dsmmval2  20924  psrmulr  21134  mplmonmul  21218  mplcoe3  21220  opsrbaslem  21231  opsrbaslemOLD  21232  opsrtoslem2  21244  psr1val  21338  ply1basfvi  21393  ply1plusgfvi  21394  psr1sca2  21403  evl1fval1lem  21477  mattpos1  21586  mdettpos  21741  smadiadetglem1  21801  tgdif0  22123  indislem  22131  restco  22296  txtopon  22723  txindislem  22765  qtopres  22830  hmphindis  22929  ptuncnv  22939  snclseqg  23248  tsmssplit  23284  ussval  23392  tuslem  23399  tuslemOLD  23400  setsmsbas  23609  setsmsbasOLD  23610  tnglemOLD  23778  tngds  23792  tngdsOLD  23793  tngtset  23794  pcoass  24168  cphsqrtcl2  24331  rrxcph  24537  ovolunlem1a  24641  ioorinv  24721  itg11  24836  itg1mulc  24850  itg2cnlem1  24907  iblss2  24951  ibladdlem  24965  itgfsum  24972  iblabslem  24973  iblabs  24974  ditgneg  25002  deg1fvi  25231  dgrco  25417  logfac  25737  cxpexp  25804  cxpmul2  25825  cxpsqrt  25839  cxpsqrtth  25865  dvcxp1  25874  dvcxp2  25875  ang180lem1  25940  mcubic  25978  quart1  25987  reasinsin  26027  atanlogaddlem  26044  atantayl2  26069  log2tlbnd  26076  basellem2  26212  basellem3  26213  basellem5  26215  basellem8  26218  dchrmulid2  26381  bcp1ctr  26408  lgsneg  26450  lgsneg1  26451  lgsdir2  26459  lgsdir  26461  lgsdi  26463  lgsquad2lem2  26514  pntleml  26740  motgrp  26885  lmiisolem  27138  ttglemOLD  27220  egrsubgr  27625  iswwlksnon  28197  iswspthsnon  28200  bafval  28945  ipidsq  29051  ipasslem1  29172  pjclem2  30537  cvmdi  30665  imadifxp  30919  2ndimaxp  30963  iundisjcnt  31098  dpfrac1  31145  gsumpart  31294  cycpmco2rn  31371  cyc3genpmlem  31397  resvsca  31508  rspectset  31795  indval2  31961  bayesth  32385  ofcccat  32501  plymulx  32506  subfacp1lem6  33126  satfdm  33310  mvtval  33441  mexval  33443  mexval2  33444  mdvval  33445  mrsubfval  33449  mrsubvrs  33463  msubfval  33465  elmsubrn  33469  mvhfval  33474  mpstval  33476  msrfval  33478  mstaval  33485  mthmval  33516  bccolsum  33684  dfrdg2  33750  dfrdg3  33751  lrold  34056  dfrdg4  34232  ordtoplem  34603  ordcmp  34615  curunc  35738  matunitlindflem2  35753  poimirlem6  35762  poimirlem7  35763  poimirlem11  35767  poimirlem12  35768  poimirlem13  35769  poimirlem14  35770  poimirlem16  35772  poimirlem19  35775  poimirlem21  35777  poimirlem22  35778  poimirlem27  35783  poimirlem31  35787  poimirlem32  35788  itg2addnclem2  35808  ibladdnclem  35812  iblabsnclem  35819  iblabsnc  35820  iblmulc2nc  35821  ftc1anclem8  35836  pmodN  37843  tgrpgrplem  38742  tendoplass  38776  tendoicl  38789  erngdvlem3  38983  dvhvaddass  39090  dib0  39157  dib1dim2  39161  diclspsn  39187  cdlemn8  39197  dihopelvalcpre  39241  djhcom  39398  nn0expgcd  40315  kelac2  40870  mendbas  40989  mendring  40997  iscard4  41102  relexp01min  41274  relexpaddss  41279  iotain  41988  addrcom  42046  rnsnf  42674  itgsinexplem1  43449  volioc  43467  dirkertrigeqlem1  43593  fourierdlem104  43705  sqwvfoura  43723  sqwvfourb  43724  fzopredsuc  44767  fppr2odd  45135  rngccatidALTV  45499  ringccatidALTV  45562  0dig2pr01  45908  nn0sumshdiglemB  45918