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 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  rabsnif  4689  uniintsn  4950  iinvdif  5046  iununi  5065  csbcnv  5872  dmxpid  5920  rnxpid  6171  csbrn  6204  dmsnsnsn  6221  opswap  6230  xpcoid  6291  predres  6340  unizlim  6485  fvco4i  6983  fndmdifcom  7038  fmptsng  7166  fmptsnd  7167  csbov  7455  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  10230  cfidm  10254  alephsing  10255  itunisuc  10398  itunitc  10400  ituniiun  10401  alephadd  10557  alephreg  10562  pwcfsdom  10563  addcompq  10930  addcomnq  10931  mulcompq  10932  mulcomnq  10933  addassnq  10938  mulassnq  10939  addrid  11385  indval2  12218  zeo  12677  xnegneg  13235  xaddcom  13261  xaddrid  13262  xnegdi  13269  xmulrid  13300  xadddilem  13315  ixxin  13384  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  16085  efexp  16152  tanval2  16184  sadeq  16525  smumullem  16545  smumul  16546  gcdcom  16566  gcd0id  16572  gcdass  16600  nn0expgcd  16617  lcmcom  16646  lcmneg  16656  lcmass  16667  nn0gcdsq  16806  dfphi2  16828  pcneg  16929  setscom  17235  strfvi  17245  fveqprc  17246  oveqprc  17247  ressbas  17291  ressinbas  17300  ressress  17302  firest  17480  topnval  17482  xpsfeq  17612  xpsaddlem  17622  xpsvsca  17626  oppchomfval  17765  rescbas  17881  rescco  17884  cofuass  17941  fucbas  18015  fuchom  18016  setccatid  18136  estrccatid  18183  xpcbas  18229  oduleval  18340  odulub  18456  oduglb  18458  ipotset  18584  efmndbas  18925  efmndbasabf  18926  symggrplem  18938  smndex1mndlem  18966  pwmnd  18994  grpinvfvi  19044  cntrval  19384  cntzval  19386  oppgplusfval  19413  snsymgefmndeq  19460  symgvalstruct  19462  pmtrprfval  19552  m1expaddsub  19563  sylow1lem2  19664  sylow3lem1  19692  oppglsm  19707  gsumzsplit  19992  gsum2dlem2  20036  gsumcom2  20040  dprd2dlem2  20107  dprd2da  20109  dmdprdsplit2lem  20112  mgpplusg  20215  mgpress  20221  ringidval  20260  opprmulfval  20417  abvtrivd  20935  sralem  21297  srasca  21301  sravsca  21302  sraip  21303  rlmval  21312  zlmsca  21670  zlmvsca  21671  psgninv  21732  ocvval  21817  thlbas  21846  thlle  21847  thloc  21849  dsmmval2  21886  psrmulr  22092  mplmonmul  22187  mplcoe3  22189  opsrbaslem  22200  opsrtoslem2  22207  psr1val  22346  ply1basfvi  22400  ply1plusgfvi  22401  psr1sca2  22410  evl1fval1lem  22490  mattpos1  22613  mdettpos  22768  smadiadetglem1  22828  tgdif0  23149  indislem  23157  restco  23321  txtopon  23748  txindislem  23790  qtopres  23855  hmphindis  23954  ptuncnv  23964  snclseqg  24273  tsmssplit  24309  ussval  24416  tuslem  24423  setsmsbas  24632  tngds  24805  tngtset  24806  pcoass  25183  cphsqrtcl2  25345  rrxcph  25551  ovolunlem1a  25655  ioorinv  25735  itg11  25850  itg1mulc  25863  itg2cnlem1  25920  iblss2  25965  ibladdlem  25979  itgfsum  25986  iblabslem  25987  iblabs  25988  ditgneg  26016  deg1fvi  26242  dgrco  26432  plymulidp  26443  logfac  26766  cxpexp  26833  cxpmul2  26854  cxpsqrt  26868  cxpsqrtth  26895  dvcxp1  26905  dvcxp2  26906  ang180lem1  26974  mcubic  27012  quart1  27021  reasinsin  27061  atanlogaddlem  27078  atantayl2  27103  log2tlbnd  27110  basellem2  27246  basellem3  27247  basellem5  27249  basellem8  27252  fsumdvdsmul  27359  dchrmullid  27416  bcp1ctr  27443  lgsneg  27485  lgsneg1  27486  lgsdir2  27494  lgsdir  27496  lgsdi  27498  lgsquad2lem2  27549  pntleml  27775  lrold  28090  abssnid  28436  om2noseqfo  28491  n0seo  28614  pw2cutp1  28654  motgrp  28812  lmiisolem  29105  egrsubgr  29627  iswwlksnon  30202  iswspthsnon  30205  bafval  30956  ipidsq  31062  ipasslem1  31183  pjclem2  32548  cvmdi  32676  imadifxp  32946  2ndimaxp  32991  suppun2  33029  iundisjcnt  33143  dpfrac1  33211  gsumpart  33383  suppgsumssiun  33392  cycpmco2rn  33445  cyc3genpmlem  33471  fracbas  33626  resvsca  33652  psrgsum  33938  psrmonmul  33940  psrmonprod  33942  rspectset  34256  bayesth  34829  ofcccat  34933  subfacp1lem6  35677  satfdm  35861  mvtval  35992  mexval  35994  mexval2  35995  mdvval  35996  mrsubfval  36000  mrsubvrs  36014  msubfval  36016  elmsubrn  36020  mvhfval  36025  mpstval  36027  msrfval  36029  mstaval  36036  mthmval  36067  bccolsum  36231  dfrdg2  36285  dfrdg3  36286  dfrdg4  36443  ordtoplem  36946  ordcmp  36958  curunc  38253  matunitlindflem2  38268  poimirlem6  38277  poimirlem7  38278  poimirlem11  38282  poimirlem12  38283  poimirlem13  38284  poimirlem14  38285  poimirlem16  38287  poimirlem19  38290  poimirlem21  38292  poimirlem22  38293  poimirlem27  38298  poimirlem31  38302  poimirlem32  38303  itg2addnclem2  38323  ibladdnclem  38327  iblabsnclem  38334  iblabsnc  38335  iblmulc2nc  38336  ftc1anclem8  38351  pmodN  40624  tgrpgrplem  41523  tendoplass  41557  tendoicl  41570  erngdvlem3  41764  dvhvaddass  41871  dib0  41938  dib1dim2  41942  diclspsn  41968  cdlemn8  41978  dihopelvalcpre  42022  djhcom  42179  evlsbagval  43318  kelac2  43792  mendbas  43907  mendring  43915  iscard4  44259  relexp01min  44439  relexpaddss  44444  iotain  45127  addrcom  45183  rnsnf  45902  limsupvaluz  46422  itgsinexplem1  46668  volioc  46686  dirkertrigeqlem1  46812  fourierdlem104  46924  sqwvfoura  46942  sqwvfourb  46943  hoicvr  47262  fzopredsuc  48061  ppivalnn  48384  fppr2odd  48496  dfnbgr5  48616  gpgprismgr4cycllem10  48869  rngccatidALTV  49037  ringccatidALTV  49071  0dig2pr01  49390  nn0sumshdiglemB  49400  imaidfu2  49889  oppczeroo  50015  dfswapf2  50039  oppc1stf  50066  oppc2ndf  50067  prcof1  50166  setc1onsubc  50380  termolmd  50448