Theorem 3eqtr4a 2798

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  rabsnif  4668  uniintsn  4928  iinvdif  5023  iununi  5042  dmxpid  5880  rnxpid  6132  csbrn  6162  dmsnsnsn  6179  opswap  6188  xpcoid  6249  predres  6298  unizlim  6442  fvco4i  6936  fndmdifcom  6990  fmptsng  7117  fmptsnd  7118  csbov  7406  ordunisuc  7777  offres  7930  1stval2  7953  2ndval2  7954  cnvf1olem  8054  fparlem3  8058  fparlem4  8059  frrlem12  8241  seqomlem1  8383  ecovcom  8764  ecovass  8765  ecovdi  8766  resixpfo  8878  mapunen  9078  cardidm  9877  cardiun  9900  alephcard  9986  cardalephex  10006  cardcf  10168  cfidm  10191  alephsing  10192  itunisuc  10335  itunitc  10337  ituniiun  10338  alephadd  10494  alephreg  10499  pwcfsdom  10500  addcompq  10867  addcomnq  10868  mulcompq  10869  mulcomnq  10870  addassnq  10875  mulassnq  10876  addrid  11320  indval2  12158  zeo  12609  xnegneg  13160  xaddcom  13186  xaddrid  13187  xnegdi  13194  xmulrid  13225  xadddilem  13240  ixxin  13309  fzsuc2  13530  expneg  14025  sq01  14181  facp1  14234  bcpasc  14277  hashfzp1  14387  resunimafz0  14401  hashf1lem1  14411  hashf1  14413  ccat1st1st  14585  swrdccatin1  14681  swrdccat3blem  14695  repswsymballbi  14736  cshwmodn  14751  cshwlen  14755  repswcshw  14768  trclun  14970  relexpcnv  14991  relexpaddd  15010  absexp  15260  sqreulem  15316  fsumf1o  15679  fsumadd  15696  fsumrev2  15738  fsumparts  15763  fsumrelem  15764  fprodf1o  15905  fprodmul  15919  fproddiv  15920  fprodfac  15932  fallfacfwd  15995  efexp  16062  tanval2  16094  sadeq  16435  smumullem  16455  smumul  16456  gcdcom  16476  gcd0id  16482  gcdass  16510  nn0expgcd  16527  lcmcom  16556  lcmneg  16566  lcmass  16577  nn0gcdsq  16716  dfphi2  16738  pcneg  16839  setscom  17144  strfvi  17154  fveqprc  17155  oveqprc  17156  ressbas  17200  ressinbas  17209  ressress  17211  firest  17389  topnval  17391  xpsfeq  17521  xpsaddlem  17531  xpsvsca  17535  oppchomfval  17674  rescbas  17790  rescco  17793  cofuass  17850  fucbas  17924  fuchom  17925  setccatid  18045  estrccatid  18092  xpcbas  18138  oduleval  18249  odulub  18365  oduglb  18367  ipotset  18493  efmndbas  18833  efmndbasabf  18834  symggrplem  18846  smndex1mndlem  18874  pwmnd  18902  grpinvfvi  18952  cntrval  19288  cntzval  19290  oppgplusfval  19317  snsymgefmndeq  19364  symgvalstruct  19366  pmtrprfval  19456  m1expaddsub  19467  sylow1lem2  19568  sylow3lem1  19596  oppglsm  19611  gsumzsplit  19896  gsum2dlem2  19940  gsumcom2  19944  dprd2dlem2  20011  dprd2da  20013  dmdprdsplit2lem  20016  mgpplusg  20119  mgpress  20125  ringidval  20158  opprmulfval  20313  abvtrivd  20803  sralem  21166  srasca  21170  sravsca  21171  sraip  21172  rlmval  21181  zlmsca  21513  zlmvsca  21514  psgninv  21575  ocvval  21660  thlbas  21689  thlle  21690  thloc  21692  dsmmval2  21729  psrmulr  21934  mplmonmul  22027  mplcoe3  22029  opsrbaslem  22040  opsrtoslem2  22047  psr1val  22162  ply1basfvi  22217  ply1plusgfvi  22218  psr1sca2  22227  evl1fval1lem  22308  mattpos1  22434  mdettpos  22589  smadiadetglem1  22649  tgdif0  22970  indislem  22978  restco  23142  txtopon  23569  txindislem  23611  qtopres  23676  hmphindis  23775  ptuncnv  23785  snclseqg  24094  tsmssplit  24130  ussval  24237  tuslem  24244  setsmsbas  24453  tngds  24626  tngtset  24627  pcoass  25004  cphsqrtcl2  25166  rrxcph  25372  ovolunlem1a  25476  ioorinv  25556  itg11  25671  itg1mulc  25684  itg2cnlem1  25741  iblss2  25786  ibladdlem  25800  itgfsum  25807  iblabslem  25808  iblabs  25809  ditgneg  25837  deg1fvi  26063  dgrco  26253  logfac  26581  cxpexp  26648  cxpmul2  26669  cxpsqrt  26683  cxpsqrtth  26710  dvcxp1  26720  dvcxp2  26721  ang180lem1  26789  mcubic  26827  quart1  26836  reasinsin  26876  atanlogaddlem  26893  atantayl2  26918  log2tlbnd  26925  basellem2  27062  basellem3  27063  basellem5  27065  basellem8  27068  fsumdvdsmul  27175  dchrmullid  27232  bcp1ctr  27259  lgsneg  27301  lgsneg1  27302  lgsdir2  27310  lgsdir  27312  lgsdi  27314  lgsquad2lem2  27365  pntleml  27591  lrold  27906  abssnid  28252  om2noseqfo  28307  n0seo  28430  pw2cutp1  28470  motgrp  28628  lmiisolem  28881  egrsubgr  29363  iswwlksnon  29939  iswspthsnon  29942  bafval  30693  ipidsq  30799  ipasslem1  30920  pjclem2  32285  cvmdi  32413  imadifxp  32689  2ndimaxp  32737  suppun2  32775  iundisjcnt  32889  dpfrac1  32969  gsumpart  33142  suppgsumssiun  33151  cycpmco2rn  33204  cyc3genpmlem  33230  fracbas  33384  resvsca  33410  psrgsum  33710  psrmonmul  33712  psrmonprod  33714  rspectset  34029  bayesth  34602  ofcccat  34706  plymulx  34711  subfacp1lem6  35386  satfdm  35570  mvtval  35701  mexval  35703  mexval2  35704  mdvval  35705  mrsubfval  35709  mrsubvrs  35723  msubfval  35725  elmsubrn  35729  mvhfval  35734  mpstval  35736  msrfval  35738  mstaval  35745  mthmval  35776  bccolsum  35940  dfrdg2  35994  dfrdg3  35995  dfrdg4  36152  ordtoplem  36636  ordcmp  36648  curunc  37940  matunitlindflem2  37955  poimirlem6  37964  poimirlem7  37965  poimirlem11  37969  poimirlem12  37970  poimirlem13  37971  poimirlem14  37972  poimirlem16  37974  poimirlem19  37977  poimirlem21  37979  poimirlem22  37980  poimirlem27  37985  poimirlem31  37989  poimirlem32  37990  itg2addnclem2  38010  ibladdnclem  38014  iblabsnclem  38021  iblabsnc  38022  iblmulc2nc  38023  ftc1anclem8  38038  pmodN  40313  tgrpgrplem  41212  tendoplass  41246  tendoicl  41259  erngdvlem3  41453  dvhvaddass  41560  dib0  41627  dib1dim2  41631  diclspsn  41657  cdlemn8  41667  dihopelvalcpre  41711  djhcom  41868  evlsbagval  43019  kelac2  43514  mendbas  43629  mendring  43637  iscard4  43981  relexp01min  44161  relexpaddss  44166  iotain  44865  addrcom  44922  rnsnf  45635  itgsinexplem1  46403  volioc  46421  dirkertrigeqlem1  46547  fourierdlem104  46659  sqwvfoura  46677  sqwvfourb  46678  hoicvr  46997  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