Theorem 3eqtr4a 2797

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 2787	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2774	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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  rabsnif  4680  uniintsn  4940  iinvdif  5035  iununi  5054  dmxpid  5879  rnxpid  6131  csbrn  6161  dmsnsnsn  6178  opswap  6187  xpcoid  6248  predres  6297  unizlim  6441  fvco4i  6935  fndmdifcom  6988  fmptsng  7114  fmptsnd  7115  csbov  7403  ordunisuc  7774  offres  7927  1stval2  7950  2ndval2  7951  cnvf1olem  8052  fparlem3  8056  fparlem4  8057  frrlem12  8239  seqomlem1  8381  ecovcom  8760  ecovass  8761  ecovdi  8762  resixpfo  8874  mapunen  9074  cardidm  9871  cardiun  9894  alephcard  9980  cardalephex  10000  cardcf  10162  cfidm  10185  alephsing  10186  itunisuc  10329  itunitc  10331  ituniiun  10332  alephadd  10488  alephreg  10493  pwcfsdom  10494  addcompq  10861  addcomnq  10862  mulcompq  10863  mulcomnq  10864  addassnq  10869  mulassnq  10870  addrid  11313  zeo  12578  xnegneg  13129  xaddcom  13155  xaddrid  13156  xnegdi  13163  xmulrid  13194  xadddilem  13209  ixxin  13278  fzsuc2  13498  expneg  13992  sq01  14148  facp1  14201  bcpasc  14244  hashfzp1  14354  resunimafz0  14368  hashf1lem1  14378  hashf1  14380  ccat1st1st  14552  swrdccatin1  14648  swrdccat3blem  14662  repswsymballbi  14703  cshwmodn  14718  cshwlen  14722  repswcshw  14735  trclun  14937  relexpcnv  14958  relexpaddd  14977  absexp  15227  sqreulem  15283  fsumf1o  15646  fsumadd  15663  fsumrev2  15705  fsumparts  15729  fsumrelem  15730  fprodf1o  15869  fprodmul  15883  fproddiv  15884  fprodfac  15896  fallfacfwd  15959  efexp  16026  tanval2  16058  sadeq  16399  smumullem  16419  smumul  16420  gcdcom  16440  gcd0id  16446  gcdass  16474  nn0expgcd  16491  lcmcom  16520  lcmneg  16530  lcmass  16541  nn0gcdsq  16679  dfphi2  16701  pcneg  16802  setscom  17107  strfvi  17117  fveqprc  17118  oveqprc  17119  ressbas  17163  ressinbas  17172  ressress  17174  firest  17352  topnval  17354  xpsfeq  17484  xpsaddlem  17494  xpsvsca  17498  oppchomfval  17637  rescbas  17753  rescco  17756  cofuass  17813  fucbas  17887  fuchom  17888  setccatid  18008  estrccatid  18055  xpcbas  18101  oduleval  18212  odulub  18328  oduglb  18330  ipotset  18456  efmndbas  18796  efmndbasabf  18797  symggrplem  18809  smndex1mndlem  18834  pwmnd  18862  grpinvfvi  18912  cntrval  19248  cntzval  19250  oppgplusfval  19277  snsymgefmndeq  19324  symgvalstruct  19326  pmtrprfval  19416  m1expaddsub  19427  sylow1lem2  19528  sylow3lem1  19556  oppglsm  19571  gsumzsplit  19856  gsum2dlem2  19900  gsumcom2  19904  dprd2dlem2  19971  dprd2da  19973  dmdprdsplit2lem  19976  mgpplusg  20079  mgpress  20085  ringidval  20118  opprmulfval  20275  abvtrivd  20765  sralem  21128  srasca  21132  sravsca  21133  sraip  21134  rlmval  21143  zlmsca  21475  zlmvsca  21476  psgninv  21537  ocvval  21622  thlbas  21651  thlle  21652  thloc  21654  dsmmval2  21691  psrmulr  21898  mplmonmul  21991  mplcoe3  21993  opsrbaslem  22004  opsrtoslem2  22011  psr1val  22126  ply1basfvi  22181  ply1plusgfvi  22182  psr1sca2  22191  evl1fval1lem  22274  mattpos1  22400  mdettpos  22555  smadiadetglem1  22615  tgdif0  22936  indislem  22944  restco  23108  txtopon  23535  txindislem  23577  qtopres  23642  hmphindis  23741  ptuncnv  23751  snclseqg  24060  tsmssplit  24096  ussval  24203  tuslem  24210  setsmsbas  24419  tngds  24592  tngtset  24593  pcoass  24980  cphsqrtcl2  25142  rrxcph  25348  ovolunlem1a  25453  ioorinv  25533  itg11  25648  itg1mulc  25661  itg2cnlem1  25718  iblss2  25763  ibladdlem  25777  itgfsum  25784  iblabslem  25785  iblabs  25786  ditgneg  25814  deg1fvi  26046  dgrco  26237  logfac  26566  cxpexp  26633  cxpmul2  26654  cxpsqrt  26668  cxpsqrtth  26695  dvcxp1  26705  dvcxp2  26706  ang180lem1  26775  mcubic  26813  quart1  26822  reasinsin  26862  atanlogaddlem  26879  atantayl2  26904  log2tlbnd  26911  basellem2  27048  basellem3  27049  basellem5  27051  basellem8  27054  fsumdvdsmul  27161  dchrmullid  27219  bcp1ctr  27246  lgsneg  27288  lgsneg1  27289  lgsdir2  27297  lgsdir  27299  lgsdi  27301  lgsquad2lem2  27352  pntleml  27578  lrold  27893  abssnid  28239  om2noseqfo  28294  n0seo  28417  pw2cutp1  28457  motgrp  28615  lmiisolem  28868  egrsubgr  29350  iswwlksnon  29926  iswspthsnon  29929  bafval  30679  ipidsq  30785  ipasslem1  30906  pjclem2  32271  cvmdi  32399  imadifxp  32676  2ndimaxp  32724  suppun2  32763  iundisjcnt  32878  indval2  32933  dpfrac1  32973  gsumpart  33146  cycpmco2rn  33207  cyc3genpmlem  33233  fracbas  33387  resvsca  33413  rspectset  34023  bayesth  34596  ofcccat  34700  plymulx  34705  subfacp1lem6  35379  satfdm  35563  mvtval  35694  mexval  35696  mexval2  35697  mdvval  35698  mrsubfval  35702  mrsubvrs  35716  msubfval  35718  elmsubrn  35722  mvhfval  35727  mpstval  35729  msrfval  35731  mstaval  35738  mthmval  35769  bccolsum  35933  dfrdg2  35987  dfrdg3  35988  dfrdg4  36145  ordtoplem  36629  ordcmp  36641  curunc  37803  matunitlindflem2  37818  poimirlem6  37827  poimirlem7  37828  poimirlem11  37832  poimirlem12  37833  poimirlem13  37834  poimirlem14  37835  poimirlem16  37837  poimirlem19  37840  poimirlem21  37842  poimirlem22  37843  poimirlem27  37848  poimirlem31  37852  poimirlem32  37853  itg2addnclem2  37873  ibladdnclem  37877  iblabsnclem  37884  iblabsnc  37885  iblmulc2nc  37886  ftc1anclem8  37901  pmodN  40110  tgrpgrplem  41009  tendoplass  41043  tendoicl  41056  erngdvlem3  41250  dvhvaddass  41357  dib0  41424  dib1dim2  41428  diclspsn  41454  cdlemn8  41464  dihopelvalcpre  41508  djhcom  41665  evlsbagval  42812  kelac2  43307  mendbas  43422  mendring  43430  iscard4  43774  relexp01min  43954  relexpaddss  43959  iotain  44658  addrcom  44715  rnsnf  45428  itgsinexplem1  46198  volioc  46216  dirkertrigeqlem1  46342  fourierdlem104  46454  sqwvfoura  46472  sqwvfourb  46473  fzopredsuc  47569  fppr2odd  47977  dfnbgr5  48097  gpgprismgr4cycllem10  48350  rngccatidALTV  48518  ringccatidALTV  48552  0dig2pr01  48856  nn0sumshdiglemB  48866  imaidfu2  49356  oppczeroo  49482  dfswapf2  49506  oppc1stf  49533  oppc2ndf  49534  prcof1  49633  setc1onsubc  49847  termolmd  49915