Theorem 3eqtr4a 2830

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

Syntax hints:   → wi 4   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  rabsnif  4691  uniintsn  4951  iinvdif  5047  iununi  5066  csbcnv  5870  dmxpid  5918  rnxpid  6169  csbrn  6202  dmsnsnsn  6219  opswap  6228  xpcoid  6289  predres  6338  unizlim  6483  fvco4i  6981  fndmdifcom  7036  fmptsng  7164  fmptsnd  7165  csbov  7453  ordunisuc  7824  offres  7976  1stval2  7999  2ndval2  8000  cnvf1olem  8101  fparlem3  8105  fparlem4  8106  frrlem12  8290  seqomlem1  8433  ecovcom  8817  ecovass  8818  ecovdi  8819  resixpfo  8930  mapunen  9130  cardidm  9941  cardiun  9964  alephcard  10050  cardalephex  10070  cardcf  10231  cfidm  10255  alephsing  10256  itunisuc  10399  itunitc  10401  ituniiun  10402  alephadd  10558  alephreg  10563  pwcfsdom  10564  addcompq  10931  addcomnq  10932  mulcompq  10933  mulcomnq  10934  addassnq  10939  mulassnq  10940  addrid  11386  indval2  12219  zeo  12678  xnegneg  13236  xaddcom  13262  xaddrid  13263  xnegdi  13270  xmulrid  13301  xadddilem  13316  ixxin  13385  fzsuc2  13606  expneg  14101  sq01  14257  facp1  14310  bcpasc  14353  hashfzp1  14464  resunimafz0  14478  hashf1lem1  14488  hashf1  14490  ccat1st1st  14662  swrdccatin1  14758  swrdccat3blem  14772  repswsymballbi  14813  cshwmodn  14828  cshwlen  14832  repswcshw  14845  trclun  15047  relexpcnv  15068  relexpaddd  15087  absexp  15351  sqreulem  15407  fsumf1o  15770  fsumadd  15787  fsumrev2  15829  fsumparts  15854  fsumrelem  15855  fprodf1o  15996  fprodmul  16010  fproddiv  16011  fprodfac  16023  fallfacfwd  16086  efexp  16153  tanval2  16185  sadeq  16526  smumullem  16546  smumul  16547  gcdcom  16567  gcd0id  16573  gcdass  16601  nn0expgcd  16618  lcmcom  16647  lcmneg  16657  lcmass  16668  nn0gcdsq  16807  dfphi2  16829  pcneg  16930  setscom  17236  strfvi  17246  fveqprc  17247  oveqprc  17248  ressbas  17292  ressinbas  17301  ressress  17303  firest  17481  topnval  17483  xpsfeq  17613  xpsaddlem  17623  xpsvsca  17627  oppchomfval  17766  rescbas  17882  rescco  17885  cofuass  17942  fucbas  18016  fuchom  18017  setccatid  18137  estrccatid  18184  xpcbas  18230  oduleval  18341  odulub  18457  oduglb  18459  ipotset  18585  efmndbas  18926  efmndbasabf  18927  symggrplem  18939  smndex1mndlem  18967  pwmnd  18995  grpinvfvi  19045  cntrval  19385  cntzval  19387  oppgplusfval  19414  snsymgefmndeq  19461  symgvalstruct  19463  pmtrprfval  19553  m1expaddsub  19564  sylow1lem2  19665  sylow3lem1  19693  oppglsm  19708  gsumzsplit  19993  gsum2dlem2  20037  gsumcom2  20041  dprd2dlem2  20108  dprd2da  20110  dmdprdsplit2lem  20113  mgpplusg  20216  mgpress  20222  ringidval  20261  opprmulfval  20417  abvtrivd  20909  sralem  21271  srasca  21275  sravsca  21276  sraip  21277  rlmval  21286  zlmsca  21635  zlmvsca  21636  psgninv  21697  ocvval  21782  thlbas  21811  thlle  21812  thloc  21814  dsmmval2  21851  psrmulr  22057  mplmonmul  22152  mplcoe3  22154  opsrbaslem  22165  opsrtoslem2  22172  psr1val  22311  ply1basfvi  22365  ply1plusgfvi  22366  psr1sca2  22375  evl1fval1lem  22455  mattpos1  22578  mdettpos  22733  smadiadetglem1  22793  tgdif0  23114  indislem  23122  restco  23286  txtopon  23713  txindislem  23755  qtopres  23820  hmphindis  23919  ptuncnv  23929  snclseqg  24238  tsmssplit  24274  ussval  24381  tuslem  24388  setsmsbas  24597  tngds  24770  tngtset  24771  pcoass  25148  cphsqrtcl2  25310  rrxcph  25516  ovolunlem1a  25620  ioorinv  25700  itg11  25815  itg1mulc  25828  itg2cnlem1  25885  iblss2  25930  ibladdlem  25944  itgfsum  25951  iblabslem  25952  iblabs  25953  ditgneg  25981  deg1fvi  26207  dgrco  26397  plymulidp  26408  logfac  26728  cxpexp  26795  cxpmul2  26816  cxpsqrt  26830  cxpsqrtth  26857  dvcxp1  26867  dvcxp2  26868  ang180lem1  26936  mcubic  26974  quart1  26983  reasinsin  27023  atanlogaddlem  27040  atantayl2  27065  log2tlbnd  27072  basellem2  27208  basellem3  27209  basellem5  27211  basellem8  27214  fsumdvdsmul  27321  dchrmullid  27378  bcp1ctr  27405  lgsneg  27447  lgsneg1  27448  lgsdir2  27456  lgsdir  27458  lgsdi  27460  lgsquad2lem2  27511  pntleml  27737  lrold  28052  abssnid  28398  om2noseqfo  28453  n0seo  28576  pw2cutp1  28616  motgrp  28774  lmiisolem  29059  egrsubgr  29564  iswwlksnon  30139  iswspthsnon  30142  bafval  30893  ipidsq  30999  ipasslem1  31120  pjclem2  32485  cvmdi  32613  imadifxp  32883  2ndimaxp  32928  suppun2  32966  iundisjcnt  33080  dpfrac1  33148  gsumpart  33320  suppgsumssiun  33329  cycpmco2rn  33382  cyc3genpmlem  33408  fracbas  33565  resvsca  33591  psrgsum  33879  psrmonmul  33881  psrmonprod  33883  rspectset  34197  bayesth  34770  ofcccat  34874  subfacp1lem6  35572  satfdm  35756  mvtval  35887  mexval  35889  mexval2  35890  mdvval  35891  mrsubfval  35895  mrsubvrs  35909  msubfval  35911  elmsubrn  35915  mvhfval  35920  mpstval  35922  msrfval  35924  mstaval  35931  mthmval  35962  bccolsum  36126  dfrdg2  36180  dfrdg3  36181  dfrdg4  36338  ordtoplem  36831  ordcmp  36843  curunc  38136  matunitlindflem2  38151  poimirlem6  38160  poimirlem7  38161  poimirlem11  38165  poimirlem12  38166  poimirlem13  38167  poimirlem14  38168  poimirlem16  38170  poimirlem19  38173  poimirlem21  38175  poimirlem22  38176  poimirlem27  38181  poimirlem31  38185  poimirlem32  38186  itg2addnclem2  38206  ibladdnclem  38210  iblabsnclem  38217  iblabsnc  38218  iblmulc2nc  38219  ftc1anclem8  38234  pmodN  40509  tgrpgrplem  41408  tendoplass  41442  tendoicl  41455  erngdvlem3  41649  dvhvaddass  41756  dib0  41823  dib1dim2  41827  diclspsn  41853  cdlemn8  41863  dihopelvalcpre  41907  djhcom  42064  evlsbagval  43205  kelac2  43679  mendbas  43794  mendring  43802  iscard4  44146  relexp01min  44326  relexpaddss  44331  iotain  45014  addrcom  45070  rnsnf  45789  limsupvaluz  46309  itgsinexplem1  46555  volioc  46573  dirkertrigeqlem1  46699  fourierdlem104  46811  sqwvfoura  46829  sqwvfourb  46830  hoicvr  47149  fzopredsuc  47945  ppivalnn  48268  fppr2odd  48380  dfnbgr5  48500  gpgprismgr4cycllem10  48753  rngccatidALTV  48921  ringccatidALTV  48955  0dig2pr01  49270  nn0sumshdiglemB  49280  imaidfu2  49769  oppczeroo  49895  dfswapf2  49919  oppc1stf  49946  oppc2ndf  49947  prcof1  50046  setc1onsubc  50260  termolmd  50328