Theorem 3eqtr4a 2796

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

Syntax hints:   → wi 4   = wceq 1539

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  rabsnif  4726  uniintsn  4990  iinvdif  5082  iununi  5101  dmxpid  5928  rnxpid  6171  csbrn  6201  dmsnsnsn  6218  opswap  6227  xpcoid  6288  predres  6339  unizlim  6486  fvco4i  6991  fndmdifcom  7043  fmptsng  7167  fmptsnd  7168  csbov  7454  ordunisuc  7822  offres  7972  1stval2  7994  2ndval2  7995  cnvf1olem  8098  fparlem3  8102  fparlem4  8103  frrlem12  8284  seqomlem1  8452  ecovcom  8819  ecovass  8820  ecovdi  8821  resixpfo  8932  mapunen  9148  cardidm  9956  cardiun  9979  alephcard  10067  cardalephex  10087  cardcf  10249  cfidm  10272  alephsing  10273  itunisuc  10416  itunitc  10418  ituniiun  10419  alephadd  10574  alephreg  10579  pwcfsdom  10580  addcompq  10947  addcomnq  10948  mulcompq  10949  mulcomnq  10950  addassnq  10955  mulassnq  10956  addrid  11398  zeo  12652  xnegneg  13197  xaddcom  13223  xaddrid  13224  xnegdi  13231  xmulrid  13262  xadddilem  13277  ixxin  13345  fzsuc2  13563  expneg  14039  sq01  14192  facp1  14242  bcpasc  14285  hashfzp1  14395  resunimafz0  14408  hashf1lem1  14419  hashf1lem1OLD  14420  hashf1  14422  ccat1st1st  14582  swrdccatin1  14679  swrdccat3blem  14693  repswsymballbi  14734  cshwmodn  14749  cshwlen  14753  repswcshw  14766  trclun  14965  relexpcnv  14986  relexpaddd  15005  absexp  15255  sqreulem  15310  fsumf1o  15673  fsumadd  15690  fsumrev2  15732  fsumparts  15756  fsumrelem  15757  fprodf1o  15894  fprodmul  15908  fproddiv  15909  fprodfac  15921  fallfacfwd  15984  efexp  16048  tanval2  16080  sadeq  16417  smumullem  16437  smumul  16438  gcdcom  16458  gcd0id  16464  gcdass  16493  lcmcom  16534  lcmneg  16544  lcmass  16555  nn0gcdsq  16692  dfphi2  16711  pcneg  16811  setscom  17117  strfvi  17127  fveqprc  17128  oveqprc  17129  setsnidOLD  17147  ressbas  17183  ressbasOLD  17184  ressinbas  17194  ressress  17197  firest  17382  topnval  17384  xpsfeq  17513  xpsaddlem  17523  xpsvsca  17527  oppchomfval  17662  oppchomfvalOLD  17663  oppcbasOLD  17668  rescbas  17780  rescbasOLD  17781  rescco  17784  resccoOLD  17785  cofuass  17843  fucbas  17916  fuchom  17917  fuchomOLD  17918  setccatid  18038  estrccatid  18087  xpcbas  18134  oduleval  18246  odulub  18364  oduglb  18366  ipotset  18490  efmndbas  18788  efmndbasabf  18789  symggrplem  18801  smndex1mndlem  18826  pwmnd  18854  grpinvfvi  18903  cntrval  19224  cntzval  19226  oppgplusfval  19253  snsymgefmndeq  19303  symgvalstruct  19305  symgvalstructOLD  19306  pmtrprfval  19396  m1expaddsub  19407  sylow1lem2  19508  sylow3lem1  19536  oppglsm  19551  gsumzsplit  19836  gsum2dlem2  19880  gsumcom2  19884  dprd2dlem2  19951  dprd2da  19953  dmdprdsplit2lem  19956  mgpplusg  20032  mgpress  20043  mgpressOLD  20044  ringidval  20077  opprmulfval  20227  abvtrivd  20591  sralem  20935  sralemOLD  20936  srasca  20943  srascaOLD  20944  sravsca  20945  sravscaOLD  20946  sraip  20947  rlmval  20958  zlmlemOLD  21286  zlmsca  21293  zlmvsca  21294  psgninv  21354  ocvval  21439  thlbas  21468  thlbasOLD  21469  thlle  21470  thlleOLD  21471  thloc  21473  dsmmval2  21510  psrmulr  21722  mplmonmul  21810  mplcoe3  21812  opsrbaslem  21823  opsrbaslemOLD  21824  opsrtoslem2  21836  psr1val  21929  ply1basfvi  21983  ply1plusgfvi  21984  psr1sca2  21993  evl1fval1lem  22069  mattpos1  22178  mdettpos  22333  smadiadetglem1  22393  tgdif0  22715  indislem  22723  restco  22888  txtopon  23315  txindislem  23357  qtopres  23422  hmphindis  23521  ptuncnv  23531  snclseqg  23840  tsmssplit  23876  ussval  23984  tuslem  23991  tuslemOLD  23992  setsmsbas  24201  setsmsbasOLD  24202  tnglemOLD  24370  tngds  24384  tngdsOLD  24385  tngtset  24386  pcoass  24771  cphsqrtcl2  24934  rrxcph  25140  ovolunlem1a  25245  ioorinv  25325  itg11  25440  itg1mulc  25454  itg2cnlem1  25511  iblss2  25555  ibladdlem  25569  itgfsum  25576  iblabslem  25577  iblabs  25578  ditgneg  25606  deg1fvi  25838  dgrco  26025  logfac  26345  cxpexp  26412  cxpmul2  26433  cxpsqrt  26447  cxpsqrtth  26474  dvcxp1  26484  dvcxp2  26485  ang180lem1  26550  mcubic  26588  quart1  26597  reasinsin  26637  atanlogaddlem  26654  atantayl2  26679  log2tlbnd  26686  basellem2  26822  basellem3  26823  basellem5  26825  basellem8  26828  dchrmullid  26991  bcp1ctr  27018  lgsneg  27060  lgsneg1  27061  lgsdir2  27069  lgsdir  27071  lgsdi  27073  lgsquad2lem2  27124  pntleml  27350  lrold  27628  motgrp  28061  lmiisolem  28314  ttglemOLD  28396  egrsubgr  28801  iswwlksnon  29374  iswspthsnon  29377  bafval  30124  ipidsq  30230  ipasslem1  30351  pjclem2  31716  cvmdi  31844  imadifxp  32099  2ndimaxp  32139  iundisjcnt  32276  dpfrac1  32325  gsumpart  32477  cycpmco2rn  32554  cyc3genpmlem  32580  resvsca  32714  rspectset  33144  indval2  33310  bayesth  33736  ofcccat  33852  plymulx  33857  subfacp1lem6  34474  satfdm  34658  mvtval  34789  mexval  34791  mexval2  34792  mdvval  34793  mrsubfval  34797  mrsubvrs  34811  msubfval  34813  elmsubrn  34817  mvhfval  34822  mpstval  34824  msrfval  34826  mstaval  34833  mthmval  34864  bccolsum  35013  dfrdg2  35071  dfrdg3  35072  dfrdg4  35227  ordtoplem  35623  ordcmp  35635  curunc  36773  matunitlindflem2  36788  poimirlem6  36797  poimirlem7  36798  poimirlem11  36802  poimirlem12  36803  poimirlem13  36804  poimirlem14  36805  poimirlem16  36807  poimirlem19  36810  poimirlem21  36812  poimirlem22  36813  poimirlem27  36818  poimirlem31  36822  poimirlem32  36823  itg2addnclem2  36843  ibladdnclem  36847  iblabsnclem  36854  iblabsnc  36855  iblmulc2nc  36856  ftc1anclem8  36871  pmodN  39024  tgrpgrplem  39923  tendoplass  39957  tendoicl  39970  erngdvlem3  40164  dvhvaddass  40271  dib0  40338  dib1dim2  40342  diclspsn  40368  cdlemn8  40378  dihopelvalcpre  40422  djhcom  40579  evlsbagval  41440  nn0expgcd  41528  kelac2  42109  mendbas  42228  mendring  42236  iscard4  42586  relexp01min  42766  relexpaddss  42771  iotain  43478  addrcom  43536  rnsnf  44181  itgsinexplem1  44968  volioc  44986  dirkertrigeqlem1  45112  fourierdlem104  45224  sqwvfoura  45242  sqwvfourb  45243  fzopredsuc  46329  fppr2odd  46697  rngccatidALTV  46975  ringccatidALTV  47038  0dig2pr01  47383  nn0sumshdiglemB  47393