Theorem 3eqtr4a 2806

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  rabsnif  4748  uniintsn  5009  iinvdif  5103  iununi  5122  dmxpid  5955  rnxpid  6204  csbrn  6234  dmsnsnsn  6251  opswap  6260  xpcoid  6321  predres  6371  unizlim  6518  fvco4i  7023  fndmdifcom  7076  fmptsng  7202  fmptsnd  7203  csbov  7493  ordunisuc  7868  offres  8024  1stval2  8047  2ndval2  8048  cnvf1olem  8151  fparlem3  8155  fparlem4  8156  frrlem12  8338  seqomlem1  8506  ecovcom  8881  ecovass  8882  ecovdi  8883  resixpfo  8994  mapunen  9212  cardidm  10028  cardiun  10051  alephcard  10139  cardalephex  10159  cardcf  10321  cfidm  10344  alephsing  10345  itunisuc  10488  itunitc  10490  ituniiun  10491  alephadd  10646  alephreg  10651  pwcfsdom  10652  addcompq  11019  addcomnq  11020  mulcompq  11021  mulcomnq  11022  addassnq  11027  mulassnq  11028  addrid  11470  zeo  12729  xnegneg  13276  xaddcom  13302  xaddrid  13303  xnegdi  13310  xmulrid  13341  xadddilem  13356  ixxin  13424  fzsuc2  13642  expneg  14120  sq01  14274  facp1  14327  bcpasc  14370  hashfzp1  14480  resunimafz0  14494  hashf1lem1  14504  hashf1  14506  ccat1st1st  14676  swrdccatin1  14773  swrdccat3blem  14787  repswsymballbi  14828  cshwmodn  14843  cshwlen  14847  repswcshw  14860  trclun  15063  relexpcnv  15084  relexpaddd  15103  absexp  15353  sqreulem  15408  fsumf1o  15771  fsumadd  15788  fsumrev2  15830  fsumparts  15854  fsumrelem  15855  fprodf1o  15994  fprodmul  16008  fproddiv  16009  fprodfac  16021  fallfacfwd  16084  efexp  16149  tanval2  16181  sadeq  16518  smumullem  16538  smumul  16539  gcdcom  16559  gcd0id  16565  gcdass  16594  nn0expgcd  16611  lcmcom  16640  lcmneg  16650  lcmass  16661  nn0gcdsq  16799  dfphi2  16821  pcneg  16921  setscom  17227  strfvi  17237  fveqprc  17238  oveqprc  17239  setsnidOLD  17257  ressbas  17293  ressbasOLD  17294  ressinbas  17304  ressress  17307  firest  17492  topnval  17494  xpsfeq  17623  xpsaddlem  17633  xpsvsca  17637  oppchomfval  17772  oppchomfvalOLD  17773  oppcbasOLD  17778  rescbas  17890  rescbasOLD  17891  rescco  17894  resccoOLD  17895  cofuass  17953  fucbas  18029  fuchom  18030  fuchomOLD  18031  setccatid  18151  estrccatid  18200  xpcbas  18247  oduleval  18359  odulub  18477  oduglb  18479  ipotset  18603  efmndbas  18906  efmndbasabf  18907  symggrplem  18919  smndex1mndlem  18944  pwmnd  18972  grpinvfvi  19022  cntrval  19359  cntzval  19361  oppgplusfval  19388  snsymgefmndeq  19436  symgvalstruct  19438  symgvalstructOLD  19439  pmtrprfval  19529  m1expaddsub  19540  sylow1lem2  19641  sylow3lem1  19669  oppglsm  19684  gsumzsplit  19969  gsum2dlem2  20013  gsumcom2  20017  dprd2dlem2  20084  dprd2da  20086  dmdprdsplit2lem  20089  mgpplusg  20165  mgpress  20176  mgpressOLD  20177  ringidval  20210  opprmulfval  20362  abvtrivd  20855  sralem  21198  sralemOLD  21199  srasca  21206  srascaOLD  21207  sravsca  21208  sravscaOLD  21209  sraip  21210  rlmval  21221  zlmlemOLD  21551  zlmsca  21558  zlmvsca  21559  psgninv  21623  ocvval  21708  thlbas  21737  thlbasOLD  21738  thlle  21739  thlleOLD  21740  thloc  21742  dsmmval2  21779  psrmulr  21985  mplmonmul  22077  mplcoe3  22079  opsrbaslem  22090  opsrbaslemOLD  22091  opsrtoslem2  22103  psr1val  22208  ply1basfvi  22263  ply1plusgfvi  22264  psr1sca2  22273  evl1fval1lem  22355  mattpos1  22483  mdettpos  22638  smadiadetglem1  22698  tgdif0  23020  indislem  23028  restco  23193  txtopon  23620  txindislem  23662  qtopres  23727  hmphindis  23826  ptuncnv  23836  snclseqg  24145  tsmssplit  24181  ussval  24289  tuslem  24296  tuslemOLD  24297  setsmsbas  24506  setsmsbasOLD  24507  tnglemOLD  24675  tngds  24689  tngdsOLD  24690  tngtset  24691  pcoass  25076  cphsqrtcl2  25239  rrxcph  25445  ovolunlem1a  25550  ioorinv  25630  itg11  25745  itg1mulc  25759  itg2cnlem1  25816  iblss2  25861  ibladdlem  25875  itgfsum  25882  iblabslem  25883  iblabs  25884  ditgneg  25912  deg1fvi  26144  dgrco  26335  logfac  26661  cxpexp  26728  cxpmul2  26749  cxpsqrt  26763  cxpsqrtth  26790  dvcxp1  26800  dvcxp2  26801  ang180lem1  26870  mcubic  26908  quart1  26917  reasinsin  26957  atanlogaddlem  26974  atantayl2  26999  log2tlbnd  27006  basellem2  27143  basellem3  27144  basellem5  27146  basellem8  27149  fsumdvdsmul  27256  dchrmullid  27314  bcp1ctr  27341  lgsneg  27383  lgsneg1  27384  lgsdir2  27392  lgsdir  27394  lgsdi  27396  lgsquad2lem2  27447  pntleml  27673  lrold  27953  abssnid  28285  om2noseqfo  28322  n0seo  28423  zs12bday  28442  motgrp  28569  lmiisolem  28822  ttglemOLD  28904  egrsubgr  29312  iswwlksnon  29886  iswspthsnon  29889  bafval  30636  ipidsq  30742  ipasslem1  30863  pjclem2  32228  cvmdi  32356  imadifxp  32623  2ndimaxp  32665  iundisjcnt  32803  dpfrac1  32856  gsumpart  33038  cycpmco2rn  33118  cyc3genpmlem  33144  fracbas  33272  resvsca  33321  rspectset  33812  indval2  33978  bayesth  34404  ofcccat  34520  plymulx  34525  subfacp1lem6  35153  satfdm  35337  mvtval  35468  mexval  35470  mexval2  35471  mdvval  35472  mrsubfval  35476  mrsubvrs  35490  msubfval  35492  elmsubrn  35496  mvhfval  35501  mpstval  35503  msrfval  35505  mstaval  35512  mthmval  35543  bccolsum  35701  dfrdg2  35759  dfrdg3  35760  dfrdg4  35915  ordtoplem  36401  ordcmp  36413  curunc  37562  matunitlindflem2  37577  poimirlem6  37586  poimirlem7  37587  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem14  37594  poimirlem16  37596  poimirlem19  37599  poimirlem21  37601  poimirlem22  37602  poimirlem27  37607  poimirlem31  37611  poimirlem32  37612  itg2addnclem2  37632  ibladdnclem  37636  iblabsnclem  37643  iblabsnc  37644  iblmulc2nc  37645  ftc1anclem8  37660  pmodN  39807  tgrpgrplem  40706  tendoplass  40740  tendoicl  40753  erngdvlem3  40947  dvhvaddass  41054  dib0  41121  dib1dim2  41125  diclspsn  41151  cdlemn8  41161  dihopelvalcpre  41205  djhcom  41362  evlsbagval  42521  kelac2  43022  mendbas  43141  mendring  43149  iscard4  43495  relexp01min  43675  relexpaddss  43680  iotain  44386  addrcom  44444  rnsnf  45091  itgsinexplem1  45875  volioc  45893  dirkertrigeqlem1  46019  fourierdlem104  46131  sqwvfoura  46149  sqwvfourb  46150  fzopredsuc  47238  fppr2odd  47605  dfnbgr5  47723  rngccatidALTV  47995  ringccatidALTV  48029  0dig2pr01  48344  nn0sumshdiglemB  48354