Theorem 3eqtr4a 2792

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

Syntax hints:   → wi 4   = wceq 1534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718

This theorem is referenced by:  rabsnif  4722  uniintsn  4987  iinvdif  5080  iununi  5099  dmxpid  5928  rnxpid  6176  csbrn  6206  dmsnsnsn  6223  opswap  6232  xpcoid  6293  predres  6344  unizlim  6491  fvco4i  6995  fndmdifcom  7048  fmptsng  7174  fmptsnd  7175  csbov  7460  ordunisuc  7833  offres  7989  1stval2  8012  2ndval2  8013  cnvf1olem  8116  fparlem3  8120  fparlem4  8121  frrlem12  8304  seqomlem1  8472  ecovcom  8844  ecovass  8845  ecovdi  8846  resixpfo  8957  mapunen  9176  cardidm  9995  cardiun  10018  alephcard  10106  cardalephex  10126  cardcf  10286  cfidm  10309  alephsing  10310  itunisuc  10453  itunitc  10455  ituniiun  10456  alephadd  10611  alephreg  10616  pwcfsdom  10617  addcompq  10984  addcomnq  10985  mulcompq  10986  mulcomnq  10987  addassnq  10992  mulassnq  10993  addrid  11435  zeo  12694  xnegneg  13241  xaddcom  13267  xaddrid  13268  xnegdi  13275  xmulrid  13306  xadddilem  13321  ixxin  13389  fzsuc2  13607  expneg  14083  sq01  14237  facp1  14290  bcpasc  14333  hashfzp1  14443  resunimafz0  14457  hashf1lem1  14468  hashf1lem1OLD  14469  hashf1  14471  ccat1st1st  14631  swrdccatin1  14728  swrdccat3blem  14742  repswsymballbi  14783  cshwmodn  14798  cshwlen  14802  repswcshw  14815  trclun  15014  relexpcnv  15035  relexpaddd  15054  absexp  15304  sqreulem  15359  fsumf1o  15722  fsumadd  15739  fsumrev2  15781  fsumparts  15805  fsumrelem  15806  fprodf1o  15943  fprodmul  15957  fproddiv  15958  fprodfac  15970  fallfacfwd  16033  efexp  16098  tanval2  16130  sadeq  16467  smumullem  16487  smumul  16488  gcdcom  16508  gcd0id  16514  gcdass  16543  nn0expgcd  16560  lcmcom  16589  lcmneg  16599  lcmass  16610  nn0gcdsq  16749  dfphi2  16771  pcneg  16871  setscom  17177  strfvi  17187  fveqprc  17188  oveqprc  17189  setsnidOLD  17207  ressbas  17243  ressbasOLD  17244  ressinbas  17254  ressress  17257  firest  17442  topnval  17444  xpsfeq  17573  xpsaddlem  17583  xpsvsca  17587  oppchomfval  17722  oppchomfvalOLD  17723  oppcbasOLD  17728  rescbas  17840  rescbasOLD  17841  rescco  17844  resccoOLD  17845  cofuass  17903  fucbas  17979  fuchom  17980  fuchomOLD  17981  setccatid  18101  estrccatid  18150  xpcbas  18197  oduleval  18309  odulub  18427  oduglb  18429  ipotset  18553  efmndbas  18856  efmndbasabf  18857  symggrplem  18869  smndex1mndlem  18894  pwmnd  18922  grpinvfvi  18972  cntrval  19309  cntzval  19311  oppgplusfval  19338  snsymgefmndeq  19388  symgvalstruct  19390  symgvalstructOLD  19391  pmtrprfval  19481  m1expaddsub  19492  sylow1lem2  19593  sylow3lem1  19621  oppglsm  19636  gsumzsplit  19921  gsum2dlem2  19965  gsumcom2  19969  dprd2dlem2  20036  dprd2da  20038  dmdprdsplit2lem  20041  mgpplusg  20117  mgpress  20128  mgpressOLD  20129  ringidval  20162  opprmulfval  20314  abvtrivd  20807  sralem  21150  sralemOLD  21151  srasca  21158  srascaOLD  21159  sravsca  21160  sravscaOLD  21161  sraip  21162  rlmval  21173  zlmlemOLD  21503  zlmsca  21510  zlmvsca  21511  psgninv  21574  ocvval  21659  thlbas  21688  thlbasOLD  21689  thlle  21690  thlleOLD  21691  thloc  21693  dsmmval2  21730  psrmulr  21947  mplmonmul  22039  mplcoe3  22041  opsrbaslem  22052  opsrbaslemOLD  22053  opsrtoslem2  22065  psr1val  22171  ply1basfvi  22226  ply1plusgfvi  22227  psr1sca2  22236  evl1fval1lem  22318  mattpos1  22446  mdettpos  22601  smadiadetglem1  22661  tgdif0  22983  indislem  22991  restco  23156  txtopon  23583  txindislem  23625  qtopres  23690  hmphindis  23789  ptuncnv  23799  snclseqg  24108  tsmssplit  24144  ussval  24252  tuslem  24259  tuslemOLD  24260  setsmsbas  24469  setsmsbasOLD  24470  tnglemOLD  24638  tngds  24652  tngdsOLD  24653  tngtset  24654  pcoass  25039  cphsqrtcl2  25202  rrxcph  25408  ovolunlem1a  25513  ioorinv  25593  itg11  25708  itg1mulc  25722  itg2cnlem1  25779  iblss2  25823  ibladdlem  25837  itgfsum  25844  iblabslem  25845  iblabs  25846  ditgneg  25874  deg1fvi  26109  dgrco  26300  logfac  26625  cxpexp  26692  cxpmul2  26713  cxpsqrt  26727  cxpsqrtth  26754  dvcxp1  26764  dvcxp2  26765  ang180lem1  26834  mcubic  26872  quart1  26881  reasinsin  26921  atanlogaddlem  26938  atantayl2  26963  log2tlbnd  26970  basellem2  27107  basellem3  27108  basellem5  27110  basellem8  27113  fsumdvdsmul  27220  dchrmullid  27278  bcp1ctr  27305  lgsneg  27347  lgsneg1  27348  lgsdir2  27356  lgsdir  27358  lgsdi  27360  lgsquad2lem2  27411  pntleml  27637  lrold  27917  abssnid  28235  om2noseqfo  28269  motgrp  28467  lmiisolem  28720  ttglemOLD  28802  egrsubgr  29210  iswwlksnon  29784  iswspthsnon  29787  bafval  30534  ipidsq  30640  ipasslem1  30761  pjclem2  32126  cvmdi  32254  imadifxp  32521  2ndimaxp  32564  iundisjcnt  32703  dpfrac1  32756  gsumpart  32927  cycpmco2rn  33007  cyc3genpmlem  33033  fracbas  33160  resvsca  33209  rspectset  33694  indval2  33860  bayesth  34286  ofcccat  34402  plymulx  34407  subfacp1lem6  35026  satfdm  35210  mvtval  35341  mexval  35343  mexval2  35344  mdvval  35345  mrsubfval  35349  mrsubvrs  35363  msubfval  35365  elmsubrn  35369  mvhfval  35374  mpstval  35376  msrfval  35378  mstaval  35385  mthmval  35416  bccolsum  35574  dfrdg2  35632  dfrdg3  35633  dfrdg4  35788  ordtoplem  36160  ordcmp  36172  curunc  37316  matunitlindflem2  37331  poimirlem6  37340  poimirlem7  37341  poimirlem11  37345  poimirlem12  37346  poimirlem13  37347  poimirlem14  37348  poimirlem16  37350  poimirlem19  37353  poimirlem21  37355  poimirlem22  37356  poimirlem27  37361  poimirlem31  37365  poimirlem32  37366  itg2addnclem2  37386  ibladdnclem  37390  iblabsnclem  37397  iblabsnc  37398  iblmulc2nc  37399  ftc1anclem8  37414  pmodN  39562  tgrpgrplem  40461  tendoplass  40495  tendoicl  40508  erngdvlem3  40702  dvhvaddass  40809  dib0  40876  dib1dim2  40880  diclspsn  40906  cdlemn8  40916  dihopelvalcpre  40960  djhcom  41117  evlsbagval  42256  kelac2  42763  mendbas  42882  mendring  42890  iscard4  43237  relexp01min  43417  relexpaddss  43422  iotain  44128  addrcom  44186  rnsnf  44827  itgsinexplem1  45611  volioc  45629  dirkertrigeqlem1  45755  fourierdlem104  45867  sqwvfoura  45885  sqwvfourb  45886  fzopredsuc  46972  fppr2odd  47339  dfnbgr5  47454  rngccatidALTV  47685  ringccatidALTV  47719  0dig2pr01  48034  nn0sumshdiglemB  48044