Theorem 3eqtr4a 2682

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	|- A = B
3eqtr4a.2	|- ( ph -> C = A )
3eqtr4a.3	|- ( ph -> D = B )

Assertion

Ref	Expression
3eqtr4a	|- ( ph -> C = D )

Proof of Theorem 3eqtr4a

Step	Hyp	Ref	Expression
1		3eqtr4a.2	. . 3 |- ( ph -> C = A )
2		3eqtr4a.1	. . 3 |- A = B
3	1, 2	syl6eq 2672	. 2 |- ( ph -> C = B )
4		3eqtr4a.3	. 2 |- ( ph -> D = B )
5	3, 4	eqtr4d 2659	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  rabsnif  4258  uniintsn  4514  iinvdif  4592  iununi  4610  dmxpid  5345  rnxpid  5567  csbrn  5596  dmsnsnsn  5613  opswap  5622  xpcoid  5676  unizlim  5844  fvco4i  6276  fndmdifcom  6322  fmptsng  6434  fmptsnd  6435  csbov  6688  ordunisuc  7032  offres  7163  1stval2  7185  2ndval2  7186  cnvf1olem  7275  fparlem3  7279  fparlem4  7280  imacosupp  7335  seqomlem1  7545  ecovcom  7854  ecovass  7855  ecovdi  7856  resixpfo  7946  mapunen  8129  cardidm  8785  cardiun  8808  alephcard  8893  cardalephex  8913  cardcf  9074  cfidm  9097  alephsing  9098  itunisuc  9241  itunitc  9243  ituniiun  9244  alephadd  9399  alephreg  9404  pwcfsdom  9405  addcompq  9772  addcomnq  9773  mulcompq  9774  mulcomnq  9775  addassnq  9780  mulassnq  9781  addid1  10216  zeo  11463  xnegneg  12045  xaddcom  12071  xaddid1  12072  xnegdi  12078  xmulid1  12109  xadddilem  12124  ixxin  12192  fzsuc2  12398  expneg  12868  sq01  12986  facp1  13065  bcpasc  13108  hashfzp1  13218  resunimafz0  13229  hashf1lem1  13239  hashf1  13241  swrdccatin1  13483  swrdccat3blem  13495  repswsymballbi  13527  cshwmodn  13541  repswcshw  13558  trclun  13755  relexpcnv  13775  absexp  14044  sqreulem  14099  fsumf1o  14454  fsumadd  14470  fsumrev2  14514  fsumparts  14538  fsumrelem  14539  pwm1geoser  14600  fprodf1o  14676  fprodmul  14690  fproddiv  14691  fprodfac  14703  fallfacfwd  14767  efexp  14831  tanval2  14863  sqrt2irrlemOLD  14978  sadeq  15194  smumullem  15214  smumul  15215  gcdcom  15235  gcd0id  15240  gcdass  15264  lcmcom  15306  lcmneg  15316  lcmass  15327  nn0gcdsq  15460  dfphi2  15479  pcneg  15578  setscom  15903  strfvi  15913  setsnid  15915  ressbas  15930  ressinbas  15936  ressress  15938  firest  16093  topnval  16095  xpsfeq  16224  xpsaddlem  16235  xpsvsca  16239  homffval  16350  oppchomfval  16374  oppcbas  16378  rescbas  16489  rescco  16492  cofuass  16549  fucbas  16620  fuchom  16621  setccatid  16734  estrccatid  16772  xpcbas  16818  xpchomfval  16819  xpccofval  16822  oduleval  17131  oduglb  17139  odulub  17141  ipotset  17157  grpinvfvi  17463  cntrval  17752  cntzval  17754  oppgplusfval  17778  symgbas  17800  symggrp  17820  pmtrprfval  17907  m1expaddsub  17918  sylow1lem2  18014  sylow3lem1  18042  oppglsm  18057  gsumzsplit  18327  gsum2dlem2  18370  gsumcom2  18374  dprd2dlem2  18439  dprd2da  18441  dmdprdsplit2lem  18444  mgpplusg  18493  mgpress  18500  ringidval  18503  opprmulfval  18625  abvtrivd  18840  sralem  19177  srasca  19181  sravsca  19182  sraip  19183  rlmval  19191  psrmulr  19384  mplmonmul  19464  mplcoe3  19466  opsrbaslem  19477  opsrbaslemOLD  19478  opsrtoslem2  19485  psr1val  19556  ply1basfvi  19611  ply1plusgfvi  19612  psr1sca2  19621  evl1fval1lem  19694  zlmlem  19865  zlmsca  19869  zlmvsca  19870  psgninv  19928  ocvval  20011  thlbas  20040  thlle  20041  thloc  20043  dsmmval2  20080  mattpos1  20262  mdettpos  20417  smadiadetglem1  20477  tgdif0  20796  indislem  20804  restco  20968  txtopon  21394  txindislem  21436  qtopres  21501  hmphindis  21600  ptuncnv  21610  snclseqg  21919  tsmssplit  21955  ussval  22063  tuslem  22071  setsmsbas  22280  tnglem  22444  tngds  22452  tngtset  22453  pcoass  22824  cphsqrtcl2  22986  rrxcph  23180  ovolunlem1a  23264  ioorinv  23344  itg11  23458  itg1mulc  23471  itg2cnlem1  23528  iblss2  23572  ibladdlem  23586  itgfsum  23593  iblabslem  23594  iblabs  23595  ditgneg  23621  deg1fvi  23845  dgrco  24031  logfac  24347  cxpexp  24414  cxpmul2  24435  cxpsqrt  24449  dvcxp1  24481  dvcxp2  24482  ang180lem1  24539  mcubic  24574  quart1  24583  reasinsin  24623  atanlogaddlem  24640  atantayl2  24665  log2tlbnd  24672  basellem2  24808  basellem3  24809  basellem5  24811  basellem8  24814  dchrmulid2  24977  bcp1ctr  25004  lgsneg  25046  lgsneg1  25047  lgsdir2  25055  lgsdir  25057  lgsdi  25059  lgsquad2lem2  25110  pntleml  25300  motgrp  25438  lmiisolem  25688  ttglem  25756  egrsubgr  26169  iswwlksnon  26740  iswspthsnon  26741  bafval  27459  ipidsq  27565  ipasslem1  27686  pjclem2  29055  cvmdi  29183  imadifxp  29414  iundisjcnt  29557  dpfrac1  29599  dpfrac1OLD  29600  resvsca  29830  indval2  30076  bayesth  30501  plymulx  30625  subfacp1lem6  31167  mvtval  31397  mexval  31399  mexval2  31400  mdvval  31401  mrsubfval  31405  mrsubvrs  31419  msubfval  31421  elmsubrn  31425  mvhfval  31430  mpstval  31432  msrfval  31434  mstaval  31441  mthmval  31472  bccolsum  31625  dfrdg2  31701  dfrdg3  31702  dfrdg4  32058  ordtoplem  32434  ordcmp  32446  curunc  33391  matunitlindflem2  33406  poimirlem6  33415  poimirlem7  33416  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem16  33425  poimirlem19  33428  poimirlem21  33430  poimirlem22  33431  poimirlem27  33436  poimirlem31  33440  poimirlem32  33441  itg2addnclem2  33462  ibladdnclem  33466  iblabsnclem  33473  iblabsnc  33474  iblmulc2nc  33475  ftc1anclem8  33492  pmodN  35136  tgrpgrplem  36037  tendoplass  36071  tendoicl  36084  erngdvlem3  36278  dvhvaddass  36386  dib0  36453  dib1dim2  36457  diclspsn  36483  cdlemn8  36493  dihopelvalcpre  36537  djhcom  36694  kelac2  37635  mendbas  37754  mendsca  37759  mendring  37762  relexp01min  38005  relexpaddss  38010  iotain  38618  addrcom  38679  itgsinexplem1  40169  volioc  40188  dirkertrigeqlem1  40315  fourierdlem104  40427  sqwvfoura  40445  sqwvfourb  40446  opidg  41297  fzopredsuc  41333  rngccatidALTV  41989  ringccatidALTV  42052  0dig2pr01  42404  nn0sumshdiglemB  42414