Theorem 3eqtr4a 2824

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  rabsnif  4686  uniintsn  4950  iinvdif  5045  iununi  5064  csbcnv  5876  dmxpid  5924  rnxpid  6183  csbrn  6223  dmsnsnsn  6240  opswap  6249  xpcoid  6319  predres  6368  unizlim  6513  iotain  6539  fvco4i  7018  fndmdifcom  7073  fmptsng  7204  fmptsnd  7205  csbov  7496  ordunisuc  7877  offres  8029  1stval2  8052  2ndval2  8053  cnvf1olem  8158  fparlem3  8162  fparlem4  8163  frrlem12  8353  seqomlem1  8498  ecovcom  8882  ecovass  8883  ecovdi  8884  resixpfo  9002  mapunen  9203  cardidm  10077  cardiun  10102  alephcard  10188  cardalephex  10208  cardcf  10368  cfidm  10392  alephsing  10393  itunisuc  10536  itunitc  10538  ituniiun  10539  alephadd  10701  alephreg  10706  pwcfsdom  10707  addcompq  11074  addcomnq  11075  mulcompq  11076  mulcomnq  11077  addassnq  11082  mulassnq  11083  addrid  11529  indval2  12365  zeo  12825  xnegneg  13384  xaddcom  13410  xaddrid  13411  xnegdi  13418  xmulrid  13449  xadddilem  13464  ixxin  13533  fzsuc2  13756  expneg  14252  sq01  14410  facp1  14463  bcpasc  14506  hashfzp1  14617  resunimafz0  14631  hashf1lem1  14641  hashf1  14643  ccat1st1st  14818  swrdccatin1  14916  swrdccat3blem  14930  repswsymballbi  14973  cshwmodn  14988  cshwlen  14992  repswcshw  15005  trclun  15210  relexpcnv  15231  relexpaddd  15250  absexp  15514  sqreulem  15571  fsumf1o  15933  fsumadd  15950  fsumrev2  15992  fsumparts  16017  fsumrelem  16018  fprodf1o  16157  fprodmul  16171  fproddiv  16172  fprodfac  16184  fallfacfwd  16246  efexp  16313  tanval2  16345  sadeq  16686  smumullem  16706  smumul  16707  gcdcom  16729  gcd0id  16735  gcdass  16764  nn0expgcd  16782  lcmcom  16812  lcmneg  16822  lcmass  16833  nn0gcdsq  16972  dfphi2  16995  pcneg  17096  setscom  17402  strfvi  17412  fveqprc  17413  oveqprc  17414  ressbas  17458  ressinbas  17467  ressress  17469  firest  17653  topnval  17655  xpsfeq  17785  xpsaddlem  17795  xpsvsca  17799  oppchomfval  17938  rescbas  18054  rescco  18057  cofuass  18114  fucbas  18188  fuchom  18189  setccatid  18309  estrccatid  18356  xpcbas  18402  oduleval  18513  odulub  18629  oduglb  18631  ipotset  18757  mgmn0plusgplusf  18878  efmndbas  19117  efmndbasabf  19118  symggrplem  19130  smndex1mndlem  19158  pwmnd  19193  grpinvfvi  19243  cntrval  19584  cntzval  19586  oppgplusfval  19613  snsymgefmndeq  19660  symgvalstruct  19662  pmtrprfval  19752  m1expaddsub  19763  sylow1lem2  19864  sylow3lem1  19892  oppglsm  19907  gsumzsplit  20192  gsum2dlem2  20236  gsumcom2  20240  dprd2dlem2  20307  dprd2da  20309  dmdprdsplit2lem  20312  mgpplusg  20415  mgpress  20421  ringidval  20460  opprmulfval  20620  abvtrivd  21140  sralem  21502  srasca  21506  sravsca  21507  sraip  21508  rlmval  21517  zlmsca  21881  zlmvsca  21882  psgninv  21943  ocvval  22028  thlbas  22057  thlle  22058  thloc  22060  dsmmval2  22097  psrmulr  22305  mplmonmul  22400  mplcoe3  22402  opsrbaslem  22413  opsrtoslem2  22420  psr1val  22559  ply1basfvi  22613  ply1plusgfvi  22614  psr1sca2  22623  evl1fval1lem  22703  mattpos1  22826  mdettpos  22981  smadiadetglem1  23041  matunitlindflem2  23050  tgdif0  23365  indislem  23373  restco  23537  txtopon  23965  txindislem  24007  qtopres  24072  hmphindis  24171  ptuncnv  24181  snclseqg  24490  tsmssplit  24526  ussval  24633  tuslem  24640  setsmsbas  24849  tngds  25022  tngtset  25023  pcoass  25400  cphsqrtcl2  25562  rrxcph  25768  ovolunlem1a  25872  ioorinv  25952  itg11  26067  itg1mulc  26080  itg2cnlem1  26137  iblss2  26181  ibladdlem  26195  itgfsum  26202  iblabslem  26203  iblabs  26204  ditgneg  26232  deg1fvi  26458  dgrco  26649  plymulidp  26658  logfac  26986  cxpexp  27053  cxpmul2  27074  cxpsqrt  27088  cxpsqrtth  27115  dvcxp1  27125  dvcxp2  27126  ang180lem1  27194  mcubic  27232  quart1  27241  reasinsin  27281  atanlogaddlem  27298  atantayl2  27323  log2tlbnd  27330  basellem2  27466  basellem3  27467  basellem5  27469  basellem8  27472  fsumdvdsmul  27579  dchrmullid  27636  bcp1ctr  27663  lgsneg  27705  lgsneg1  27706  lgsdir2  27714  lgsdir  27716  lgsdi  27718  lgsquad2lem2  27769  pntleml  27995  lrold  28340  abssnid  28686  om2noseqfo  28741  n0seo  28864  pw2cutp1  28904  motgrp  29063  lmiisolem  29358  egrsubgr  29915  iswwlksnon  30499  iswspthsnon  30502  bafval  31263  ipidsq  31369  ipasslem1  31490  pjclem2  32855  cvmdi  32983  imadifxp  33293  2ndimaxp  33338  suppun2  33374  iundisjcnt  33486  dpfrac1  33554  gsumpart  33723  suppgsumssiun  33732  cycpmco2rn  33785  cyc3genpmlem  33811  fracbas  33971  resvsca  33997  psrgsum  34291  psrmonmul  34293  psrmonprod  34295  rspectset  34609  bayesth  35182  ofcccat  35286  subfacp1lem6  36158  satfdm  36342  mvtval  36473  mexval  36475  mexval2  36476  mdvval  36477  mrsubfval  36481  mrsubvrs  36495  msubfval  36497  elmsubrn  36501  mvhfval  36506  mpstval  36508  msrfval  36510  mstaval  36517  mthmval  36548  bccolsum  36719  dfrdg2  36772  dfrdg3  36773  dfrdg4  36930  ordtoplem  37438  ordcmp  37450  curunc  38793  poimirlem6  38812  poimirlem7  38813  poimirlem11  38817  poimirlem12  38818  poimirlem13  38819  poimirlem14  38820  poimirlem16  38822  poimirlem19  38825  poimirlem21  38827  poimirlem22  38828  poimirlem27  38833  poimirlem31  38837  poimirlem32  38838  itg2addnclem2  38858  ibladdnclem  38862  iblabsnclem  38869  iblabsnc  38870  iblmulc2nc  38871  ftc1anclem8  38886  pmodN  41173  tgrpgrplem  42072  tendoplass  42106  tendoicl  42119  erngdvlem3  42313  dvhvaddass  42420  dib0  42487  dib1dim2  42491  diclspsn  42517  cdlemn8  42527  dihopelvalcpre  42571  djhcom  42728  evlsbagval  43880  kelac2  44333  mendbas  44443  mendring  44451  iscard4  44795  relexp01min  44974  relexpaddss  44979  addrcom  45717  rnsnf  46472  limsupvaluz  46991  itgsinexplem1  47237  volioc  47255  dirkertrigeqlem1  47381  fourierdlem104  47493  sqwvfoura  47511  sqwvfourb  47512  hoicvr  47831  fzopredsuc  48667  ppivalnn  48990  fppr2odd  49102  dfnbgr5  49222  gpgprismgr4cycllem10  49475  rngccatidALTV  49642  ringccatidALTV  49676  0dig2pr01  50053  nn0sumshdiglemB  50063  imaidfu2  50558  oppczeroo  50690  dfswapf2  50714  oppc1stf  50741  oppc2ndf  50742  prcof1  50854  setc1onsubc  51071  parcatid2  51094  parcatid  51095  parmapfunc2  51105  parmapfunc  51106  termolmd  51184