Theorem 3eqtr4a 2821

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  rabsnif  4680  uniintsn  4944  iinvdif  5039  iununi  5058  csbcnv  5865  dmxpid  5913  rnxpid  6167  csbrn  6207  dmsnsnsn  6224  opswap  6233  xpcoid  6296  predres  6345  unizlim  6490  iotain  6516  fvco4i  6992  fndmdifcom  7047  fmptsng  7177  fmptsnd  7178  csbov  7469  ordunisuc  7847  offres  7999  1stval2  8022  2ndval2  8023  cnvf1olem  8127  fparlem3  8131  fparlem4  8132  frrlem12  8322  seqomlem1  8467  ecovcom  8851  ecovass  8852  ecovdi  8853  resixpfo  8971  mapunen  9172  cardidm  10047  cardiun  10070  alephcard  10156  cardalephex  10176  cardcf  10336  cfidm  10360  alephsing  10361  itunisuc  10504  itunitc  10506  ituniiun  10507  alephadd  10669  alephreg  10674  pwcfsdom  10675  addcompq  11042  addcomnq  11043  mulcompq  11044  mulcomnq  11045  addassnq  11050  mulassnq  11051  addrid  11497  indval2  12332  zeo  12792  xnegneg  13351  xaddcom  13377  xaddrid  13378  xnegdi  13385  xmulrid  13416  xadddilem  13431  ixxin  13500  fzsuc2  13723  expneg  14219  sq01  14376  facp1  14429  bcpasc  14472  hashfzp1  14583  resunimafz0  14597  hashf1lem1  14607  hashf1  14609  ccat1st1st  14784  swrdccatin1  14882  swrdccat3blem  14896  repswsymballbi  14939  cshwmodn  14954  cshwlen  14958  repswcshw  14971  trclun  15176  relexpcnv  15197  relexpaddd  15216  absexp  15480  sqreulem  15536  fsumf1o  15898  fsumadd  15915  fsumrev2  15957  fsumparts  15982  fsumrelem  15983  fprodf1o  16122  fprodmul  16136  fproddiv  16137  fprodfac  16149  fallfacfwd  16211  efexp  16278  tanval2  16310  sadeq  16651  smumullem  16671  smumul  16672  gcdcom  16694  gcd0id  16700  gcdass  16729  nn0expgcd  16747  lcmcom  16777  lcmneg  16787  lcmass  16798  nn0gcdsq  16937  dfphi2  16960  pcneg  17061  setscom  17367  strfvi  17377  fveqprc  17378  oveqprc  17379  ressbas  17423  ressinbas  17432  ressress  17434  firest  17612  topnval  17614  xpsfeq  17744  xpsaddlem  17754  xpsvsca  17758  oppchomfval  17897  rescbas  18013  rescco  18016  cofuass  18073  fucbas  18147  fuchom  18148  setccatid  18268  estrccatid  18315  xpcbas  18361  oduleval  18472  odulub  18588  oduglb  18590  ipotset  18716  mgmn0plusgplusf  18837  efmndbas  19076  efmndbasabf  19077  symggrplem  19089  smndex1mndlem  19117  pwmnd  19152  grpinvfvi  19202  cntrval  19542  cntzval  19544  oppgplusfval  19571  snsymgefmndeq  19618  symgvalstruct  19620  pmtrprfval  19710  m1expaddsub  19721  sylow1lem2  19822  sylow3lem1  19850  oppglsm  19865  gsumzsplit  20150  gsum2dlem2  20194  gsumcom2  20198  dprd2dlem2  20265  dprd2da  20267  dmdprdsplit2lem  20270  mgpplusg  20373  mgpress  20379  ringidval  20418  opprmulfval  20578  abvtrivd  21098  sralem  21460  srasca  21464  sravsca  21465  sraip  21466  rlmval  21475  zlmsca  21835  zlmvsca  21836  psgninv  21897  ocvval  21982  thlbas  22011  thlle  22012  thloc  22014  dsmmval2  22051  psrmulr  22259  mplmonmul  22354  mplcoe3  22356  opsrbaslem  22367  opsrtoslem2  22374  psr1val  22513  ply1basfvi  22567  ply1plusgfvi  22568  psr1sca2  22577  evl1fval1lem  22657  mattpos1  22780  mdettpos  22935  smadiadetglem1  22995  matunitlindflem2  23004  tgdif0  23319  indislem  23327  restco  23491  txtopon  23919  txindislem  23961  qtopres  24026  hmphindis  24125  ptuncnv  24135  snclseqg  24444  tsmssplit  24480  ussval  24587  tuslem  24594  setsmsbas  24803  tngds  24976  tngtset  24977  pcoass  25354  cphsqrtcl2  25516  rrxcph  25722  ovolunlem1a  25826  ioorinv  25906  itg11  26021  itg1mulc  26034  itg2cnlem1  26091  iblss2  26135  ibladdlem  26149  itgfsum  26156  iblabslem  26157  iblabs  26158  ditgneg  26186  deg1fvi  26412  dgrco  26603  plymulidp  26612  logfac  26938  cxpexp  27005  cxpmul2  27026  cxpsqrt  27040  cxpsqrtth  27067  dvcxp1  27077  dvcxp2  27078  ang180lem1  27146  mcubic  27184  quart1  27193  reasinsin  27233  atanlogaddlem  27250  atantayl2  27275  log2tlbnd  27282  basellem2  27418  basellem3  27419  basellem5  27421  basellem8  27424  fsumdvdsmul  27531  dchrmullid  27588  bcp1ctr  27615  lgsneg  27657  lgsneg1  27658  lgsdir2  27666  lgsdir  27668  lgsdi  27670  lgsquad2lem2  27721  pntleml  27947  lrold  28292  abssnid  28638  om2noseqfo  28693  n0seo  28816  pw2cutp1  28856  motgrp  29015  lmiisolem  29310  egrsubgr  29867  iswwlksnon  30451  iswspthsnon  30454  bafval  31215  ipidsq  31321  ipasslem1  31442  pjclem2  32807  cvmdi  32935  imadifxp  33246  2ndimaxp  33291  suppun2  33328  iundisjcnt  33440  dpfrac1  33508  gsumpart  33674  suppgsumssiun  33683  cycpmco2rn  33736  cyc3genpmlem  33762  fracbas  33917  resvsca  33943  psrgsum  34230  psrmonmul  34232  psrmonprod  34234  rspectset  34548  bayesth  35121  ofcccat  35225  subfacp1lem6  36040  satfdm  36224  mvtval  36355  mexval  36357  mexval2  36358  mdvval  36359  mrsubfval  36363  mrsubvrs  36377  msubfval  36379  elmsubrn  36383  mvhfval  36388  mpstval  36390  msrfval  36392  mstaval  36399  mthmval  36430  bccolsum  36600  dfrdg2  36653  dfrdg3  36654  dfrdg4  36811  ordtoplem  37319  ordcmp  37331  curunc  38634  poimirlem6  38653  poimirlem7  38654  poimirlem11  38658  poimirlem12  38659  poimirlem13  38660  poimirlem14  38661  poimirlem16  38663  poimirlem19  38666  poimirlem21  38668  poimirlem22  38669  poimirlem27  38674  poimirlem31  38678  poimirlem32  38679  itg2addnclem2  38699  ibladdnclem  38703  iblabsnclem  38710  iblabsnc  38711  iblmulc2nc  38712  ftc1anclem8  38727  pmodN  41016  tgrpgrplem  41915  tendoplass  41949  tendoicl  41962  erngdvlem3  42156  dvhvaddass  42263  dib0  42330  dib1dim2  42334  diclspsn  42360  cdlemn8  42370  dihopelvalcpre  42414  djhcom  42571  evlsbagval  43723  kelac2  44176  mendbas  44291  mendring  44299  iscard4  44643  relexp01min  44822  relexpaddss  44827  addrcom  45565  rnsnf  46307  limsupvaluz  46826  itgsinexplem1  47072  volioc  47090  dirkertrigeqlem1  47216  fourierdlem104  47328  sqwvfoura  47346  sqwvfourb  47347  hoicvr  47666  fzopredsuc  48502  ppivalnn  48825  fppr2odd  48937  dfnbgr5  49057  gpgprismgr4cycllem10  49310  rngccatidALTV  49477  ringccatidALTV  49511  0dig2pr01  49830  nn0sumshdiglemB  49840  imaidfu2  50335  oppczeroo  50467  dfswapf2  50491  oppc1stf  50518  oppc2ndf  50519  prcof1  50631  setc1onsubc  50848  parcatid2  50871  parcatid  50872  parmapfunc2  50882  parmapfunc  50883  termolmd  50961