Theorem 3eqtr4a 2800

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

Syntax hints:   → wi 4   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  rabsnif  4655  uniintsn  4915  iinvdif  5009  iununi  5028  dmxpid  5872  rnxpid  6124  csbrn  6154  dmsnsnsn  6171  opswap  6180  xpcoid  6241  predres  6290  unizlim  6434  fvco4i  6929  fndmdifcom  6984  fmptsng  7112  fmptsnd  7113  csbov  7401  ordunisuc  7772  offres  7925  1stval2  7948  2ndval2  7949  cnvf1olem  8049  fparlem3  8053  fparlem4  8054  frrlem12  8237  seqomlem1  8379  ecovcom  8760  ecovass  8761  ecovdi  8762  resixpfo  8874  mapunen  9074  cardidm  9874  cardiun  9897  alephcard  9983  cardalephex  10003  cardcf  10165  cfidm  10188  alephsing  10189  itunisuc  10332  itunitc  10334  ituniiun  10335  alephadd  10491  alephreg  10496  pwcfsdom  10497  addcompq  10864  addcomnq  10865  mulcompq  10866  mulcomnq  10867  addassnq  10872  mulassnq  10873  addrid  11317  indval2  12155  zeo  12606  xnegneg  13157  xaddcom  13183  xaddrid  13184  xnegdi  13191  xmulrid  13222  xadddilem  13237  ixxin  13306  fzsuc2  13527  expneg  14022  sq01  14178  facp1  14231  bcpasc  14274  hashfzp1  14384  resunimafz0  14398  hashf1lem1  14408  hashf1  14410  ccat1st1st  14582  swrdccatin1  14678  swrdccat3blem  14692  repswsymballbi  14733  cshwmodn  14748  cshwlen  14752  repswcshw  14765  trclun  14967  relexpcnv  14988  relexpaddd  15007  absexp  15257  sqreulem  15313  fsumf1o  15676  fsumadd  15693  fsumrev2  15735  fsumparts  15760  fsumrelem  15761  fprodf1o  15902  fprodmul  15916  fproddiv  15917  fprodfac  15929  fallfacfwd  15992  efexp  16059  tanval2  16091  sadeq  16432  smumullem  16452  smumul  16453  gcdcom  16473  gcd0id  16479  gcdass  16507  nn0expgcd  16524  lcmcom  16553  lcmneg  16563  lcmass  16574  nn0gcdsq  16713  dfphi2  16735  pcneg  16836  setscom  17141  strfvi  17151  fveqprc  17152  oveqprc  17153  ressbas  17197  ressinbas  17206  ressress  17208  firest  17386  topnval  17388  xpsfeq  17518  xpsaddlem  17528  xpsvsca  17532  oppchomfval  17671  rescbas  17787  rescco  17790  cofuass  17847  fucbas  17921  fuchom  17922  setccatid  18042  estrccatid  18089  xpcbas  18135  oduleval  18246  odulub  18362  oduglb  18364  ipotset  18490  efmndbas  18830  efmndbasabf  18831  symggrplem  18843  smndex1mndlem  18871  pwmnd  18899  grpinvfvi  18949  cntrval  19285  cntzval  19287  oppgplusfval  19314  snsymgefmndeq  19361  symgvalstruct  19363  pmtrprfval  19453  m1expaddsub  19464  sylow1lem2  19565  sylow3lem1  19593  oppglsm  19608  gsumzsplit  19893  gsum2dlem2  19937  gsumcom2  19941  dprd2dlem2  20008  dprd2da  20010  dmdprdsplit2lem  20013  mgpplusg  20116  mgpress  20122  ringidval  20155  opprmulfval  20310  abvtrivd  20804  sralem  21166  srasca  21170  sravsca  21171  sraip  21172  rlmval  21181  zlmsca  21495  zlmvsca  21496  psgninv  21557  ocvval  21642  thlbas  21671  thlle  21672  thloc  21674  dsmmval2  21711  psrmulr  21917  mplmonmul  22012  mplcoe3  22014  opsrbaslem  22025  opsrtoslem2  22032  psr1val  22171  ply1basfvi  22225  ply1plusgfvi  22226  psr1sca2  22235  evl1fval1lem  22316  mattpos1  22439  mdettpos  22594  smadiadetglem1  22654  tgdif0  22975  indislem  22983  restco  23147  txtopon  23574  txindislem  23616  qtopres  23681  hmphindis  23780  ptuncnv  23790  snclseqg  24099  tsmssplit  24135  ussval  24242  tuslem  24249  setsmsbas  24458  tngds  24631  tngtset  24632  pcoass  25009  cphsqrtcl2  25171  rrxcph  25377  ovolunlem1a  25481  ioorinv  25561  itg11  25676  itg1mulc  25689  itg2cnlem1  25746  iblss2  25791  ibladdlem  25805  itgfsum  25812  iblabslem  25813  iblabs  25814  ditgneg  25842  deg1fvi  26068  dgrco  26258  logfac  26583  cxpexp  26650  cxpmul2  26671  cxpsqrt  26685  cxpsqrtth  26712  dvcxp1  26722  dvcxp2  26723  ang180lem1  26791  mcubic  26829  quart1  26838  reasinsin  26878  atanlogaddlem  26895  atantayl2  26920  log2tlbnd  26927  basellem2  27063  basellem3  27064  basellem5  27066  basellem8  27069  fsumdvdsmul  27176  dchrmullid  27233  bcp1ctr  27260  lgsneg  27302  lgsneg1  27303  lgsdir2  27311  lgsdir  27313  lgsdi  27315  lgsquad2lem2  27366  pntleml  27592  lrold  27907  abssnid  28253  om2noseqfo  28308  n0seo  28431  pw2cutp1  28471  motgrp  28629  lmiisolem  28882  egrsubgr  29364  iswwlksnon  29939  iswspthsnon  29942  bafval  30693  ipidsq  30799  ipasslem1  30920  pjclem2  32285  cvmdi  32413  imadifxp  32690  2ndimaxp  32738  suppun2  32776  iundisjcnt  32890  dpfrac1  32970  gsumpart  33144  suppgsumssiun  33153  cycpmco2rn  33206  cyc3genpmlem  33232  fracbas  33389  resvsca  33415  psrgsum  33732  psrmonmul  33734  psrmonprod  33736  rspectset  34050  bayesth  34623  ofcccat  34727  plymulx  34732  subfacp1lem6  35413  satfdm  35597  mvtval  35728  mexval  35730  mexval2  35731  mdvval  35732  mrsubfval  35736  mrsubvrs  35750  msubfval  35752  elmsubrn  35756  mvhfval  35761  mpstval  35763  msrfval  35765  mstaval  35772  mthmval  35803  bccolsum  35967  dfrdg2  36021  dfrdg3  36022  dfrdg4  36179  ordtoplem  36663  ordcmp  36675  curunc  37969  matunitlindflem2  37984  poimirlem6  37993  poimirlem7  37994  poimirlem11  37998  poimirlem12  37999  poimirlem13  38000  poimirlem14  38001  poimirlem16  38003  poimirlem19  38006  poimirlem21  38008  poimirlem22  38009  poimirlem27  38014  poimirlem31  38018  poimirlem32  38019  itg2addnclem2  38039  ibladdnclem  38043  iblabsnclem  38050  iblabsnc  38051  iblmulc2nc  38052  ftc1anclem8  38067  pmodN  40342  tgrpgrplem  41241  tendoplass  41275  tendoicl  41288  erngdvlem3  41482  dvhvaddass  41589  dib0  41656  dib1dim2  41660  diclspsn  41686  cdlemn8  41696  dihopelvalcpre  41740  djhcom  41897  evlsbagval  43036  kelac2  43510  mendbas  43625  mendring  43633  iscard4  43977  relexp01min  44157  relexpaddss  44162  iotain  44861  addrcom  44918  rnsnf  45631  itgsinexplem1  46397  volioc  46415  dirkertrigeqlem1  46541  fourierdlem104  46653  sqwvfoura  46671  sqwvfourb  46672  hoicvr  46991  fzopredsuc  47787  ppivalnn  48110  fppr2odd  48222  dfnbgr5  48342  gpgprismgr4cycllem10  48595  rngccatidALTV  48763  ringccatidALTV  48797  0dig2pr01  49101  nn0sumshdiglemB  49111  imaidfu2  49601  oppczeroo  49727  dfswapf2  49751  oppc1stf  49778  oppc2ndf  49779  prcof1  49878  setc1onsubc  50092  termolmd  50160