Theorem 3eqtr4a 2821

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752

This theorem is used by:  rabsnif  4684  uniintsn  4945  iinvdif  5040  iununi  5059  csbcnv  5866  dmxpid  5914  rnxpid  6166  csbrn  6199  dmsnsnsn  6216  opswap  6225  xpcoid  6288  predres  6337  unizlim  6482  fvco4i  6980  fndmdifcom  7035  fmptsng  7166  fmptsnd  7167  csbov  7458  ordunisuc  7828  offres  7980  1stval2  8003  2ndval2  8004  cnvf1olem  8107  fparlem3  8111  fparlem4  8112  frrlem12  8296  seqomlem1  8439  ecovcom  8823  ecovass  8824  ecovdi  8825  resixpfo  8943  mapunen  9144  cardidm  9964  cardiun  9987  alephcard  10073  cardalephex  10093  cardcf  10253  cfidm  10277  alephsing  10278  itunisuc  10421  itunitc  10423  ituniiun  10424  alephadd  10586  alephreg  10591  pwcfsdom  10592  addcompq  10959  addcomnq  10960  mulcompq  10961  mulcomnq  10962  addassnq  10967  mulassnq  10968  addrid  11414  indval2  12247  zeo  12707  xnegneg  13266  xaddcom  13292  xaddrid  13293  xnegdi  13300  xmulrid  13331  xadddilem  13346  ixxin  13415  fzsuc2  13637  expneg  14133  sq01  14289  facp1  14342  bcpasc  14385  hashfzp1  14496  resunimafz0  14510  hashf1lem1  14520  hashf1  14522  ccat1st1st  14696  swrdccatin1  14794  swrdccat3blem  14808  repswsymballbi  14851  cshwmodn  14866  cshwlen  14870  repswcshw  14883  trclun  15087  relexpcnv  15108  relexpaddd  15127  absexp  15391  sqreulem  15447  fsumf1o  15809  fsumadd  15826  fsumrev2  15868  fsumparts  15893  fsumrelem  15894  fprodf1o  16033  fprodmul  16047  fproddiv  16048  fprodfac  16060  fallfacfwd  16122  efexp  16189  tanval2  16221  sadeq  16562  smumullem  16582  smumul  16583  gcdcom  16603  gcd0id  16609  gcdass  16637  nn0expgcd  16654  lcmcom  16683  lcmneg  16693  lcmass  16704  nn0gcdsq  16843  dfphi2  16865  pcneg  16966  setscom  17272  strfvi  17282  fveqprc  17283  oveqprc  17284  ressbas  17328  ressinbas  17337  ressress  17339  firest  17517  topnval  17519  xpsfeq  17649  xpsaddlem  17659  xpsvsca  17663  oppchomfval  17802  rescbas  17918  rescco  17921  cofuass  17978  fucbas  18052  fuchom  18053  setccatid  18173  estrccatid  18220  xpcbas  18266  oduleval  18377  odulub  18493  oduglb  18495  ipotset  18621  mgmn0plusgplusf  18742  efmndbas  18980  efmndbasabf  18981  symggrplem  18993  smndex1mndlem  19021  pwmnd  19056  grpinvfvi  19106  cntrval  19446  cntzval  19448  oppgplusfval  19475  snsymgefmndeq  19522  symgvalstruct  19524  pmtrprfval  19614  m1expaddsub  19625  sylow1lem2  19726  sylow3lem1  19754  oppglsm  19769  gsumzsplit  20054  gsum2dlem2  20098  gsumcom2  20102  dprd2dlem2  20169  dprd2da  20171  dmdprdsplit2lem  20174  mgpplusg  20277  mgpress  20283  ringidval  20322  opprmulfval  20480  abvtrivd  20998  sralem  21360  srasca  21364  sravsca  21365  sraip  21366  rlmval  21375  zlmsca  21733  zlmvsca  21734  psgninv  21795  ocvval  21880  thlbas  21909  thlle  21910  thloc  21912  dsmmval2  21949  psrmulr  22157  mplmonmul  22252  mplcoe3  22254  opsrbaslem  22265  opsrtoslem2  22272  psr1val  22411  ply1basfvi  22465  ply1plusgfvi  22466  psr1sca2  22475  evl1fval1lem  22555  mattpos1  22678  mdettpos  22833  smadiadetglem1  22893  matunitlindflem2  22902  tgdif0  23217  indislem  23225  restco  23389  txtopon  23817  txindislem  23859  qtopres  23924  hmphindis  24023  ptuncnv  24033  snclseqg  24342  tsmssplit  24378  ussval  24485  tuslem  24492  setsmsbas  24701  tngds  24874  tngtset  24875  pcoass  25252  cphsqrtcl2  25414  rrxcph  25620  ovolunlem1a  25724  ioorinv  25804  itg11  25919  itg1mulc  25932  itg2cnlem1  25989  iblss2  26033  ibladdlem  26047  itgfsum  26054  iblabslem  26055  iblabs  26056  ditgneg  26084  deg1fvi  26310  dgrco  26501  plymulidp  26512  logfac  26838  cxpexp  26905  cxpmul2  26926  cxpsqrt  26940  cxpsqrtth  26967  dvcxp1  26977  dvcxp2  26978  ang180lem1  27046  mcubic  27084  quart1  27093  reasinsin  27133  atanlogaddlem  27150  atantayl2  27175  log2tlbnd  27182  basellem2  27318  basellem3  27319  basellem5  27321  basellem8  27324  fsumdvdsmul  27431  dchrmullid  27488  bcp1ctr  27515  lgsneg  27557  lgsneg1  27558  lgsdir2  27566  lgsdir  27568  lgsdi  27570  lgsquad2lem2  27621  pntleml  27847  lrold  28162  abssnid  28508  om2noseqfo  28563  n0seo  28686  pw2cutp1  28726  motgrp  28885  lmiisolem  29180  egrsubgr  29737  iswwlksnon  30321  iswspthsnon  30324  bafval  31085  ipidsq  31191  ipasslem1  31312  pjclem2  32677  cvmdi  32805  imadifxp  33074  2ndimaxp  33119  suppun2  33156  iundisjcnt  33269  dpfrac1  33337  gsumpart  33503  suppgsumssiun  33512  cycpmco2rn  33565  cyc3genpmlem  33591  fracbas  33746  resvsca  33772  psrgsum  34058  psrmonmul  34060  psrmonprod  34062  rspectset  34376  bayesth  34950  ofcccat  35054  subfacp1lem6  35764  satfdm  35948  mvtval  36079  mexval  36081  mexval2  36082  mdvval  36083  mrsubfval  36087  mrsubvrs  36101  msubfval  36103  elmsubrn  36107  mvhfval  36112  mpstval  36114  msrfval  36116  mstaval  36123  mthmval  36154  bccolsum  36318  dfrdg2  36372  dfrdg3  36373  dfrdg4  36530  ordtoplem  37054  ordcmp  37066  curunc  38356  poimirlem6  38375  poimirlem7  38376  poimirlem11  38380  poimirlem12  38381  poimirlem13  38382  poimirlem14  38383  poimirlem16  38385  poimirlem19  38388  poimirlem21  38390  poimirlem22  38391  poimirlem27  38396  poimirlem31  38400  poimirlem32  38401  itg2addnclem2  38421  ibladdnclem  38425  iblabsnclem  38432  iblabsnc  38433  iblmulc2nc  38434  ftc1anclem8  38449  pmodN  40723  tgrpgrplem  41622  tendoplass  41656  tendoicl  41669  erngdvlem3  41863  dvhvaddass  41970  dib0  42037  dib1dim2  42041  diclspsn  42067  cdlemn8  42077  dihopelvalcpre  42121  djhcom  42278  evlsbagval  43432  kelac2  43906  mendbas  44021  mendring  44029  iscard4  44373  relexp01min  44553  relexpaddss  44558  iotain  45241  addrcom  45297  rnsnf  46016  limsupvaluz  46536  itgsinexplem1  46782  volioc  46800  dirkertrigeqlem1  46926  fourierdlem104  47038  sqwvfoura  47056  sqwvfourb  47057  hoicvr  47376  fzopredsuc  48212  ppivalnn  48535  fppr2odd  48647  dfnbgr5  48767  gpgprismgr4cycllem10  49020  rngccatidALTV  49187  ringccatidALTV  49221  0dig2pr01  49540  nn0sumshdiglemB  49550  imaidfu2  50037  oppczeroo  50163  dfswapf2  50187  oppc1stf  50214  oppc2ndf  50215  prcof1  50314  setc1onsubc  50528  termolmd  50596