Theorem 3eqtr4a 2791

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  rabsnif  4690  uniintsn  4952  iinvdif  5047  iununi  5066  dmxpid  5897  rnxpid  6149  csbrn  6179  dmsnsnsn  6196  opswap  6205  xpcoid  6266  predres  6315  unizlim  6460  fvco4i  6965  fndmdifcom  7018  fmptsng  7145  fmptsnd  7146  csbov  7435  ordunisuc  7810  offres  7965  1stval2  7988  2ndval2  7989  cnvf1olem  8092  fparlem3  8096  fparlem4  8097  frrlem12  8279  seqomlem1  8421  ecovcom  8799  ecovass  8800  ecovdi  8801  resixpfo  8912  mapunen  9116  cardidm  9919  cardiun  9942  alephcard  10030  cardalephex  10050  cardcf  10212  cfidm  10235  alephsing  10236  itunisuc  10379  itunitc  10381  ituniiun  10382  alephadd  10537  alephreg  10542  pwcfsdom  10543  addcompq  10910  addcomnq  10911  mulcompq  10912  mulcomnq  10913  addassnq  10918  mulassnq  10919  addrid  11361  zeo  12627  xnegneg  13181  xaddcom  13207  xaddrid  13208  xnegdi  13215  xmulrid  13246  xadddilem  13261  ixxin  13330  fzsuc2  13550  expneg  14041  sq01  14197  facp1  14250  bcpasc  14293  hashfzp1  14403  resunimafz0  14417  hashf1lem1  14427  hashf1  14429  ccat1st1st  14600  swrdccatin1  14697  swrdccat3blem  14711  repswsymballbi  14752  cshwmodn  14767  cshwlen  14771  repswcshw  14784  trclun  14987  relexpcnv  15008  relexpaddd  15027  absexp  15277  sqreulem  15333  fsumf1o  15696  fsumadd  15713  fsumrev2  15755  fsumparts  15779  fsumrelem  15780  fprodf1o  15919  fprodmul  15933  fproddiv  15934  fprodfac  15946  fallfacfwd  16009  efexp  16076  tanval2  16108  sadeq  16449  smumullem  16469  smumul  16470  gcdcom  16490  gcd0id  16496  gcdass  16524  nn0expgcd  16541  lcmcom  16570  lcmneg  16580  lcmass  16591  nn0gcdsq  16729  dfphi2  16751  pcneg  16852  setscom  17157  strfvi  17167  fveqprc  17168  oveqprc  17169  ressbas  17213  ressinbas  17222  ressress  17224  firest  17402  topnval  17404  xpsfeq  17533  xpsaddlem  17543  xpsvsca  17547  oppchomfval  17682  rescbas  17798  rescco  17801  cofuass  17858  fucbas  17932  fuchom  17933  setccatid  18053  estrccatid  18100  xpcbas  18146  oduleval  18257  odulub  18373  oduglb  18375  ipotset  18499  efmndbas  18805  efmndbasabf  18806  symggrplem  18818  smndex1mndlem  18843  pwmnd  18871  grpinvfvi  18921  cntrval  19258  cntzval  19260  oppgplusfval  19287  snsymgefmndeq  19332  symgvalstruct  19334  pmtrprfval  19424  m1expaddsub  19435  sylow1lem2  19536  sylow3lem1  19564  oppglsm  19579  gsumzsplit  19864  gsum2dlem2  19908  gsumcom2  19912  dprd2dlem2  19979  dprd2da  19981  dmdprdsplit2lem  19984  mgpplusg  20060  mgpress  20066  ringidval  20099  opprmulfval  20255  abvtrivd  20748  sralem  21090  srasca  21094  sravsca  21095  sraip  21096  rlmval  21105  zlmsca  21437  zlmvsca  21438  psgninv  21498  ocvval  21583  thlbas  21612  thlle  21613  thloc  21615  dsmmval2  21652  psrmulr  21858  mplmonmul  21950  mplcoe3  21952  opsrbaslem  21963  opsrtoslem2  21970  psr1val  22077  ply1basfvi  22132  ply1plusgfvi  22133  psr1sca2  22142  evl1fval1lem  22224  mattpos1  22350  mdettpos  22505  smadiadetglem1  22565  tgdif0  22886  indislem  22894  restco  23058  txtopon  23485  txindislem  23527  qtopres  23592  hmphindis  23691  ptuncnv  23701  snclseqg  24010  tsmssplit  24046  ussval  24154  tuslem  24161  setsmsbas  24370  tngds  24543  tngtset  24544  pcoass  24931  cphsqrtcl2  25093  rrxcph  25299  ovolunlem1a  25404  ioorinv  25484  itg11  25599  itg1mulc  25612  itg2cnlem1  25669  iblss2  25714  ibladdlem  25728  itgfsum  25735  iblabslem  25736  iblabs  25737  ditgneg  25765  deg1fvi  25997  dgrco  26188  logfac  26517  cxpexp  26584  cxpmul2  26605  cxpsqrt  26619  cxpsqrtth  26646  dvcxp1  26656  dvcxp2  26657  ang180lem1  26726  mcubic  26764  quart1  26773  reasinsin  26813  atanlogaddlem  26830  atantayl2  26855  log2tlbnd  26862  basellem2  26999  basellem3  27000  basellem5  27002  basellem8  27005  fsumdvdsmul  27112  dchrmullid  27170  bcp1ctr  27197  lgsneg  27239  lgsneg1  27240  lgsdir2  27248  lgsdir  27250  lgsdi  27252  lgsquad2lem2  27303  pntleml  27529  lrold  27815  abssnid  28152  om2noseqfo  28199  n0seo  28314  pw2cutp1  28343  zs12bday  28350  motgrp  28477  lmiisolem  28730  egrsubgr  29211  iswwlksnon  29790  iswspthsnon  29793  bafval  30540  ipidsq  30646  ipasslem1  30767  pjclem2  32132  cvmdi  32260  imadifxp  32537  2ndimaxp  32577  suppun2  32614  iundisjcnt  32728  indval2  32784  dpfrac1  32819  gsumpart  33004  cycpmco2rn  33089  cyc3genpmlem  33115  fracbas  33262  resvsca  33311  rspectset  33863  bayesth  34437  ofcccat  34541  plymulx  34546  subfacp1lem6  35179  satfdm  35363  mvtval  35494  mexval  35496  mexval2  35497  mdvval  35498  mrsubfval  35502  mrsubvrs  35516  msubfval  35518  elmsubrn  35522  mvhfval  35527  mpstval  35529  msrfval  35531  mstaval  35538  mthmval  35569  bccolsum  35733  dfrdg2  35790  dfrdg3  35791  dfrdg4  35946  ordtoplem  36430  ordcmp  36442  curunc  37603  matunitlindflem2  37618  poimirlem6  37627  poimirlem7  37628  poimirlem11  37632  poimirlem12  37633  poimirlem13  37634  poimirlem14  37635  poimirlem16  37637  poimirlem19  37640  poimirlem21  37642  poimirlem22  37643  poimirlem27  37648  poimirlem31  37652  poimirlem32  37653  itg2addnclem2  37673  ibladdnclem  37677  iblabsnclem  37684  iblabsnc  37685  iblmulc2nc  37686  ftc1anclem8  37701  pmodN  39851  tgrpgrplem  40750  tendoplass  40784  tendoicl  40797  erngdvlem3  40991  dvhvaddass  41098  dib0  41165  dib1dim2  41169  diclspsn  41195  cdlemn8  41205  dihopelvalcpre  41249  djhcom  41406  evlsbagval  42561  kelac2  43061  mendbas  43176  mendring  43184  iscard4  43529  relexp01min  43709  relexpaddss  43714  iotain  44413  addrcom  44471  rnsnf  45185  itgsinexplem1  45959  volioc  45977  dirkertrigeqlem1  46103  fourierdlem104  46215  sqwvfoura  46233  sqwvfourb  46234  fzopredsuc  47328  fppr2odd  47736  dfnbgr5  47855  gpgprismgr4cycllem10  48098  rngccatidALTV  48264  ringccatidALTV  48298  0dig2pr01  48603  nn0sumshdiglemB  48613  imaidfu2  49104  oppczeroo  49230  dfswapf2  49254  oppc1stf  49281  oppc2ndf  49282  prcof1  49381  setc1onsubc  49595  termolmd  49663