Theorem 3eqtr4a 2790

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  rabsnif  4683  uniintsn  4945  iinvdif  5039  iununi  5058  dmxpid  5883  rnxpid  6134  csbrn  6164  dmsnsnsn  6181  opswap  6190  xpcoid  6251  predres  6300  unizlim  6445  fvco4i  6944  fndmdifcom  6997  fmptsng  7124  fmptsnd  7125  csbov  7414  ordunisuc  7787  offres  7941  1stval2  7964  2ndval2  7965  cnvf1olem  8066  fparlem3  8070  fparlem4  8071  frrlem12  8253  seqomlem1  8395  ecovcom  8773  ecovass  8774  ecovdi  8775  resixpfo  8886  mapunen  9087  cardidm  9888  cardiun  9911  alephcard  9999  cardalephex  10019  cardcf  10181  cfidm  10204  alephsing  10205  itunisuc  10348  itunitc  10350  ituniiun  10351  alephadd  10506  alephreg  10511  pwcfsdom  10512  addcompq  10879  addcomnq  10880  mulcompq  10881  mulcomnq  10882  addassnq  10887  mulassnq  10888  addrid  11330  zeo  12596  xnegneg  13150  xaddcom  13176  xaddrid  13177  xnegdi  13184  xmulrid  13215  xadddilem  13230  ixxin  13299  fzsuc2  13519  expneg  14010  sq01  14166  facp1  14219  bcpasc  14262  hashfzp1  14372  resunimafz0  14386  hashf1lem1  14396  hashf1  14398  ccat1st1st  14569  swrdccatin1  14666  swrdccat3blem  14680  repswsymballbi  14721  cshwmodn  14736  cshwlen  14740  repswcshw  14753  trclun  14956  relexpcnv  14977  relexpaddd  14996  absexp  15246  sqreulem  15302  fsumf1o  15665  fsumadd  15682  fsumrev2  15724  fsumparts  15748  fsumrelem  15749  fprodf1o  15888  fprodmul  15902  fproddiv  15903  fprodfac  15915  fallfacfwd  15978  efexp  16045  tanval2  16077  sadeq  16418  smumullem  16438  smumul  16439  gcdcom  16459  gcd0id  16465  gcdass  16493  nn0expgcd  16510  lcmcom  16539  lcmneg  16549  lcmass  16560  nn0gcdsq  16698  dfphi2  16720  pcneg  16821  setscom  17126  strfvi  17136  fveqprc  17137  oveqprc  17138  ressbas  17182  ressinbas  17191  ressress  17193  firest  17371  topnval  17373  xpsfeq  17502  xpsaddlem  17512  xpsvsca  17516  oppchomfval  17655  rescbas  17771  rescco  17774  cofuass  17831  fucbas  17905  fuchom  17906  setccatid  18026  estrccatid  18073  xpcbas  18119  oduleval  18230  odulub  18346  oduglb  18348  ipotset  18474  efmndbas  18780  efmndbasabf  18781  symggrplem  18793  smndex1mndlem  18818  pwmnd  18846  grpinvfvi  18896  cntrval  19233  cntzval  19235  oppgplusfval  19262  snsymgefmndeq  19309  symgvalstruct  19311  pmtrprfval  19401  m1expaddsub  19412  sylow1lem2  19513  sylow3lem1  19541  oppglsm  19556  gsumzsplit  19841  gsum2dlem2  19885  gsumcom2  19889  dprd2dlem2  19956  dprd2da  19958  dmdprdsplit2lem  19961  mgpplusg  20064  mgpress  20070  ringidval  20103  opprmulfval  20259  abvtrivd  20752  sralem  21115  srasca  21119  sravsca  21120  sraip  21121  rlmval  21130  zlmsca  21462  zlmvsca  21463  psgninv  21524  ocvval  21609  thlbas  21638  thlle  21639  thloc  21641  dsmmval2  21678  psrmulr  21884  mplmonmul  21976  mplcoe3  21978  opsrbaslem  21989  opsrtoslem2  21996  psr1val  22103  ply1basfvi  22158  ply1plusgfvi  22159  psr1sca2  22168  evl1fval1lem  22250  mattpos1  22376  mdettpos  22531  smadiadetglem1  22591  tgdif0  22912  indislem  22920  restco  23084  txtopon  23511  txindislem  23553  qtopres  23618  hmphindis  23717  ptuncnv  23727  snclseqg  24036  tsmssplit  24072  ussval  24180  tuslem  24187  setsmsbas  24396  tngds  24569  tngtset  24570  pcoass  24957  cphsqrtcl2  25119  rrxcph  25325  ovolunlem1a  25430  ioorinv  25510  itg11  25625  itg1mulc  25638  itg2cnlem1  25695  iblss2  25740  ibladdlem  25754  itgfsum  25761  iblabslem  25762  iblabs  25763  ditgneg  25791  deg1fvi  26023  dgrco  26214  logfac  26543  cxpexp  26610  cxpmul2  26631  cxpsqrt  26645  cxpsqrtth  26672  dvcxp1  26682  dvcxp2  26683  ang180lem1  26752  mcubic  26790  quart1  26799  reasinsin  26839  atanlogaddlem  26856  atantayl2  26881  log2tlbnd  26888  basellem2  27025  basellem3  27026  basellem5  27028  basellem8  27031  fsumdvdsmul  27138  dchrmullid  27196  bcp1ctr  27223  lgsneg  27265  lgsneg1  27266  lgsdir2  27274  lgsdir  27276  lgsdi  27278  lgsquad2lem2  27329  pntleml  27555  lrold  27846  abssnid  28185  om2noseqfo  28232  n0seo  28348  pw2cutp1  28384  zs12bday  28396  motgrp  28523  lmiisolem  28776  egrsubgr  29257  iswwlksnon  29833  iswspthsnon  29836  bafval  30583  ipidsq  30689  ipasslem1  30810  pjclem2  32175  cvmdi  32303  imadifxp  32580  2ndimaxp  32620  suppun2  32657  iundisjcnt  32771  indval2  32827  dpfrac1  32862  gsumpart  33040  cycpmco2rn  33097  cyc3genpmlem  33123  fracbas  33271  resvsca  33297  rspectset  33849  bayesth  34423  ofcccat  34527  plymulx  34532  subfacp1lem6  35165  satfdm  35349  mvtval  35480  mexval  35482  mexval2  35483  mdvval  35484  mrsubfval  35488  mrsubvrs  35502  msubfval  35504  elmsubrn  35508  mvhfval  35513  mpstval  35515  msrfval  35517  mstaval  35524  mthmval  35555  bccolsum  35719  dfrdg2  35776  dfrdg3  35777  dfrdg4  35932  ordtoplem  36416  ordcmp  36428  curunc  37589  matunitlindflem2  37604  poimirlem6  37613  poimirlem7  37614  poimirlem11  37618  poimirlem12  37619  poimirlem13  37620  poimirlem14  37621  poimirlem16  37623  poimirlem19  37626  poimirlem21  37628  poimirlem22  37629  poimirlem27  37634  poimirlem31  37638  poimirlem32  37639  itg2addnclem2  37659  ibladdnclem  37663  iblabsnclem  37670  iblabsnc  37671  iblmulc2nc  37672  ftc1anclem8  37687  pmodN  39837  tgrpgrplem  40736  tendoplass  40770  tendoicl  40783  erngdvlem3  40977  dvhvaddass  41084  dib0  41151  dib1dim2  41155  diclspsn  41181  cdlemn8  41191  dihopelvalcpre  41235  djhcom  41392  evlsbagval  42547  kelac2  43047  mendbas  43162  mendring  43170  iscard4  43515  relexp01min  43695  relexpaddss  43700  iotain  44399  addrcom  44457  rnsnf  45171  itgsinexplem1  45945  volioc  45963  dirkertrigeqlem1  46089  fourierdlem104  46201  sqwvfoura  46219  sqwvfourb  46220  fzopredsuc  47317  fppr2odd  47725  dfnbgr5  47844  gpgprismgr4cycllem10  48087  rngccatidALTV  48253  ringccatidALTV  48287  0dig2pr01  48592  nn0sumshdiglemB  48602  imaidfu2  49093  oppczeroo  49219  dfswapf2  49243  oppc1stf  49270  oppc2ndf  49271  prcof1  49370  setc1onsubc  49584  termolmd  49652