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  17651  rescbas  17767  rescco  17770  cofuass  17827  fucbas  17901  fuchom  17902  setccatid  18022  estrccatid  18069  xpcbas  18115  oduleval  18226  odulub  18342  oduglb  18344  ipotset  18468  efmndbas  18774  efmndbasabf  18775  symggrplem  18787  smndex1mndlem  18812  pwmnd  18840  grpinvfvi  18890  cntrval  19227  cntzval  19229  oppgplusfval  19256  snsymgefmndeq  19301  symgvalstruct  19303  pmtrprfval  19393  m1expaddsub  19404  sylow1lem2  19505  sylow3lem1  19533  oppglsm  19548  gsumzsplit  19833  gsum2dlem2  19877  gsumcom2  19881  dprd2dlem2  19948  dprd2da  19950  dmdprdsplit2lem  19953  mgpplusg  20029  mgpress  20035  ringidval  20068  opprmulfval  20224  abvtrivd  20717  sralem  21059  srasca  21063  sravsca  21064  sraip  21065  rlmval  21074  zlmsca  21406  zlmvsca  21407  psgninv  21467  ocvval  21552  thlbas  21581  thlle  21582  thloc  21584  dsmmval2  21621  psrmulr  21827  mplmonmul  21919  mplcoe3  21921  opsrbaslem  21932  opsrtoslem2  21939  psr1val  22046  ply1basfvi  22101  ply1plusgfvi  22102  psr1sca2  22111  evl1fval1lem  22193  mattpos1  22319  mdettpos  22474  smadiadetglem1  22534  tgdif0  22855  indislem  22863  restco  23027  txtopon  23454  txindislem  23496  qtopres  23561  hmphindis  23660  ptuncnv  23670  snclseqg  23979  tsmssplit  24015  ussval  24123  tuslem  24130  setsmsbas  24339  tngds  24512  tngtset  24513  pcoass  24900  cphsqrtcl2  25062  rrxcph  25268  ovolunlem1a  25373  ioorinv  25453  itg11  25568  itg1mulc  25581  itg2cnlem1  25638  iblss2  25683  ibladdlem  25697  itgfsum  25704  iblabslem  25705  iblabs  25706  ditgneg  25734  deg1fvi  25966  dgrco  26157  logfac  26486  cxpexp  26553  cxpmul2  26574  cxpsqrt  26588  cxpsqrtth  26615  dvcxp1  26625  dvcxp2  26626  ang180lem1  26695  mcubic  26733  quart1  26742  reasinsin  26782  atanlogaddlem  26799  atantayl2  26824  log2tlbnd  26831  basellem2  26968  basellem3  26969  basellem5  26971  basellem8  26974  fsumdvdsmul  27081  dchrmullid  27139  bcp1ctr  27166  lgsneg  27208  lgsneg1  27209  lgsdir2  27217  lgsdir  27219  lgsdi  27221  lgsquad2lem2  27272  pntleml  27498  lrold  27784  abssnid  28121  om2noseqfo  28168  n0seo  28283  pw2cutp1  28312  zs12bday  28319  motgrp  28446  lmiisolem  28699  egrsubgr  29180  iswwlksnon  29756  iswspthsnon  29759  bafval  30506  ipidsq  30612  ipasslem1  30733  pjclem2  32098  cvmdi  32226  imadifxp  32503  2ndimaxp  32543  suppun2  32580  iundisjcnt  32694  indval2  32750  dpfrac1  32785  gsumpart  32970  cycpmco2rn  33055  cyc3genpmlem  33081  fracbas  33228  resvsca  33277  rspectset  33829  bayesth  34403  ofcccat  34507  plymulx  34512  subfacp1lem6  35145  satfdm  35329  mvtval  35460  mexval  35462  mexval2  35463  mdvval  35464  mrsubfval  35468  mrsubvrs  35482  msubfval  35484  elmsubrn  35488  mvhfval  35493  mpstval  35495  msrfval  35497  mstaval  35504  mthmval  35535  bccolsum  35699  dfrdg2  35756  dfrdg3  35757  dfrdg4  35912  ordtoplem  36396  ordcmp  36408  curunc  37569  matunitlindflem2  37584  poimirlem6  37593  poimirlem7  37594  poimirlem11  37598  poimirlem12  37599  poimirlem13  37600  poimirlem14  37601  poimirlem16  37603  poimirlem19  37606  poimirlem21  37608  poimirlem22  37609  poimirlem27  37614  poimirlem31  37618  poimirlem32  37619  itg2addnclem2  37639  ibladdnclem  37643  iblabsnclem  37650  iblabsnc  37651  iblmulc2nc  37652  ftc1anclem8  37667  pmodN  39817  tgrpgrplem  40716  tendoplass  40750  tendoicl  40763  erngdvlem3  40957  dvhvaddass  41064  dib0  41131  dib1dim2  41135  diclspsn  41161  cdlemn8  41171  dihopelvalcpre  41215  djhcom  41372  evlsbagval  42527  kelac2  43027  mendbas  43142  mendring  43150  iscard4  43495  relexp01min  43675  relexpaddss  43680  iotain  44379  addrcom  44437  rnsnf  45151  itgsinexplem1  45925  volioc  45943  dirkertrigeqlem1  46069  fourierdlem104  46181  sqwvfoura  46199  sqwvfourb  46200  fzopredsuc  47297  fppr2odd  47705  dfnbgr5  47824  gpgprismgr4cycllem10  48067  rngccatidALTV  48233  ringccatidALTV  48267  0dig2pr01  48572  nn0sumshdiglemB  48582  imaidfu2  49073  oppczeroo  49199  dfswapf2  49223  oppc1stf  49250  oppc2ndf  49251  prcof1  49350  setc1onsubc  49564  termolmd  49632