Theorem 3eqtr4a 2795

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

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

This theorem is referenced by:  rabsnif  4678  uniintsn  4938  iinvdif  5033  iununi  5052  dmxpid  5877  rnxpid  6129  csbrn  6159  dmsnsnsn  6176  opswap  6185  xpcoid  6246  predres  6295  unizlim  6439  fvco4i  6933  fndmdifcom  6986  fmptsng  7112  fmptsnd  7113  csbov  7401  ordunisuc  7772  offres  7925  1stval2  7948  2ndval2  7949  cnvf1olem  8050  fparlem3  8054  fparlem4  8055  frrlem12  8237  seqomlem1  8379  ecovcom  8758  ecovass  8759  ecovdi  8760  resixpfo  8872  mapunen  9072  cardidm  9869  cardiun  9892  alephcard  9978  cardalephex  9998  cardcf  10160  cfidm  10183  alephsing  10184  itunisuc  10327  itunitc  10329  ituniiun  10330  alephadd  10486  alephreg  10491  pwcfsdom  10492  addcompq  10859  addcomnq  10860  mulcompq  10861  mulcomnq  10862  addassnq  10867  mulassnq  10868  addrid  11311  zeo  12576  xnegneg  13127  xaddcom  13153  xaddrid  13154  xnegdi  13161  xmulrid  13192  xadddilem  13207  ixxin  13276  fzsuc2  13496  expneg  13990  sq01  14146  facp1  14199  bcpasc  14242  hashfzp1  14352  resunimafz0  14366  hashf1lem1  14376  hashf1  14378  ccat1st1st  14550  swrdccatin1  14646  swrdccat3blem  14660  repswsymballbi  14701  cshwmodn  14716  cshwlen  14720  repswcshw  14733  trclun  14935  relexpcnv  14956  relexpaddd  14975  absexp  15225  sqreulem  15281  fsumf1o  15644  fsumadd  15661  fsumrev2  15703  fsumparts  15727  fsumrelem  15728  fprodf1o  15867  fprodmul  15881  fproddiv  15882  fprodfac  15894  fallfacfwd  15957  efexp  16024  tanval2  16056  sadeq  16397  smumullem  16417  smumul  16418  gcdcom  16438  gcd0id  16444  gcdass  16472  nn0expgcd  16489  lcmcom  16518  lcmneg  16528  lcmass  16539  nn0gcdsq  16677  dfphi2  16699  pcneg  16800  setscom  17105  strfvi  17115  fveqprc  17116  oveqprc  17117  ressbas  17161  ressinbas  17170  ressress  17172  firest  17350  topnval  17352  xpsfeq  17482  xpsaddlem  17492  xpsvsca  17496  oppchomfval  17635  rescbas  17751  rescco  17754  cofuass  17811  fucbas  17885  fuchom  17886  setccatid  18006  estrccatid  18053  xpcbas  18099  oduleval  18210  odulub  18326  oduglb  18328  ipotset  18454  efmndbas  18794  efmndbasabf  18795  symggrplem  18807  smndex1mndlem  18832  pwmnd  18860  grpinvfvi  18910  cntrval  19246  cntzval  19248  oppgplusfval  19275  snsymgefmndeq  19322  symgvalstruct  19324  pmtrprfval  19414  m1expaddsub  19425  sylow1lem2  19526  sylow3lem1  19554  oppglsm  19569  gsumzsplit  19854  gsum2dlem2  19898  gsumcom2  19902  dprd2dlem2  19969  dprd2da  19971  dmdprdsplit2lem  19974  mgpplusg  20077  mgpress  20083  ringidval  20116  opprmulfval  20273  abvtrivd  20763  sralem  21126  srasca  21130  sravsca  21131  sraip  21132  rlmval  21141  zlmsca  21473  zlmvsca  21474  psgninv  21535  ocvval  21620  thlbas  21649  thlle  21650  thloc  21652  dsmmval2  21689  psrmulr  21896  mplmonmul  21989  mplcoe3  21991  opsrbaslem  22002  opsrtoslem2  22009  psr1val  22124  ply1basfvi  22179  ply1plusgfvi  22180  psr1sca2  22189  evl1fval1lem  22272  mattpos1  22398  mdettpos  22553  smadiadetglem1  22613  tgdif0  22934  indislem  22942  restco  23106  txtopon  23533  txindislem  23575  qtopres  23640  hmphindis  23739  ptuncnv  23749  snclseqg  24058  tsmssplit  24094  ussval  24201  tuslem  24208  setsmsbas  24417  tngds  24590  tngtset  24591  pcoass  24978  cphsqrtcl2  25140  rrxcph  25346  ovolunlem1a  25451  ioorinv  25531  itg11  25646  itg1mulc  25659  itg2cnlem1  25716  iblss2  25761  ibladdlem  25775  itgfsum  25782  iblabslem  25783  iblabs  25784  ditgneg  25812  deg1fvi  26044  dgrco  26235  logfac  26564  cxpexp  26631  cxpmul2  26652  cxpsqrt  26666  cxpsqrtth  26693  dvcxp1  26703  dvcxp2  26704  ang180lem1  26773  mcubic  26811  quart1  26820  reasinsin  26860  atanlogaddlem  26877  atantayl2  26902  log2tlbnd  26909  basellem2  27046  basellem3  27047  basellem5  27049  basellem8  27052  fsumdvdsmul  27159  dchrmullid  27217  bcp1ctr  27244  lgsneg  27286  lgsneg1  27287  lgsdir2  27295  lgsdir  27297  lgsdi  27299  lgsquad2lem2  27350  pntleml  27576  lrold  27869  abssnid  28211  om2noseqfo  28259  n0seo  28379  pw2cutp1  28418  zs12bday  28433  motgrp  28564  lmiisolem  28817  egrsubgr  29299  iswwlksnon  29875  iswspthsnon  29878  bafval  30628  ipidsq  30734  ipasslem1  30855  pjclem2  32220  cvmdi  32348  imadifxp  32625  2ndimaxp  32673  suppun2  32712  iundisjcnt  32827  indval2  32882  dpfrac1  32922  gsumpart  33095  cycpmco2rn  33156  cyc3genpmlem  33182  fracbas  33336  resvsca  33362  rspectset  33972  bayesth  34545  ofcccat  34649  plymulx  34654  subfacp1lem6  35328  satfdm  35512  mvtval  35643  mexval  35645  mexval2  35646  mdvval  35647  mrsubfval  35651  mrsubvrs  35665  msubfval  35667  elmsubrn  35671  mvhfval  35676  mpstval  35678  msrfval  35680  mstaval  35687  mthmval  35718  bccolsum  35882  dfrdg2  35936  dfrdg3  35937  dfrdg4  36094  ordtoplem  36578  ordcmp  36590  curunc  37742  matunitlindflem2  37757  poimirlem6  37766  poimirlem7  37767  poimirlem11  37771  poimirlem12  37772  poimirlem13  37773  poimirlem14  37774  poimirlem16  37776  poimirlem19  37779  poimirlem21  37781  poimirlem22  37782  poimirlem27  37787  poimirlem31  37791  poimirlem32  37792  itg2addnclem2  37812  ibladdnclem  37816  iblabsnclem  37823  iblabsnc  37824  iblmulc2nc  37825  ftc1anclem8  37840  pmodN  40049  tgrpgrplem  40948  tendoplass  40982  tendoicl  40995  erngdvlem3  41189  dvhvaddass  41296  dib0  41363  dib1dim2  41367  diclspsn  41393  cdlemn8  41403  dihopelvalcpre  41447  djhcom  41604  evlsbagval  42754  kelac2  43249  mendbas  43364  mendring  43372  iscard4  43716  relexp01min  43896  relexpaddss  43901  iotain  44600  addrcom  44657  rnsnf  45370  itgsinexplem1  46140  volioc  46158  dirkertrigeqlem1  46284  fourierdlem104  46396  sqwvfoura  46414  sqwvfourb  46415  fzopredsuc  47511  fppr2odd  47919  dfnbgr5  48039  gpgprismgr4cycllem10  48292  rngccatidALTV  48460  ringccatidALTV  48494  0dig2pr01  48798  nn0sumshdiglemB  48808  imaidfu2  49298  oppczeroo  49424  dfswapf2  49448  oppc1stf  49475  oppc2ndf  49476  prcof1  49575  setc1onsubc  49789  termolmd  49857