Theorem 3eqtr4a 2885

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

Syntax hints:   → wi 4   = wceq 1536

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 1969  ax-7 2014  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817

This theorem is referenced by:  rabsnif  4662  uniintsn  4916  iinvdif  5005  iununi  5024  dmxpid  5803  rnxpid  6033  csbrn  6063  dmsnsnsn  6080  opswap  6089  xpcoid  6144  unizlim  6310  fvco4i  6765  fndmdifcom  6816  fmptsng  6933  fmptsnd  6934  csbov  7202  ordunisuc  7550  offres  7687  1stval2  7709  2ndval2  7710  cnvf1olem  7808  fparlem3  7812  fparlem4  7813  imacosuppOLD  7878  seqomlem1  8089  ecovcom  8406  ecovass  8407  ecovdi  8408  resixpfo  8503  mapunen  8689  cardidm  9391  cardiun  9414  alephcard  9499  cardalephex  9519  cardcf  9677  cfidm  9700  alephsing  9701  itunisuc  9844  itunitc  9846  ituniiun  9847  alephadd  10002  alephreg  10007  pwcfsdom  10008  addcompq  10375  addcomnq  10376  mulcompq  10377  mulcomnq  10378  addassnq  10383  mulassnq  10384  addid1  10823  zeo  12071  xnegneg  12610  xaddcom  12636  xaddid1  12637  xnegdi  12644  xmulid1  12675  xadddilem  12690  ixxin  12758  fzsuc2  12968  expneg  13440  sq01  13589  facp1  13641  bcpasc  13684  hashfzp1  13795  resunimafz0  13806  hashf1lem1  13816  hashf1  13818  ccat1st1st  13987  swrdccatin1  14090  swrdccat3blem  14104  repswsymballbi  14145  cshwmodn  14160  cshwlen  14164  repswcshw  14177  trclun  14377  relexpcnv  14397  absexp  14667  sqreulem  14722  fsumf1o  15083  fsumadd  15099  fsumrev2  15140  fsumparts  15164  fsumrelem  15165  pwm1geoserOLD  15228  fprodf1o  15303  fprodmul  15317  fproddiv  15318  fprodfac  15330  fallfacfwd  15393  efexp  15457  tanval2  15489  sadeq  15824  smumullem  15844  smumul  15845  gcdcom  15865  gcd0id  15870  gcdass  15898  lcmcom  15940  lcmneg  15950  lcmass  15961  nn0gcdsq  16095  dfphi2  16114  pcneg  16213  setscom  16530  strfvi  16540  setsnid  16542  ressbas  16557  ressinbas  16563  ressress  16565  firest  16709  topnval  16711  xpsfeq  16839  xpsaddlem  16849  xpsvsca  16853  oppchomfval  16987  oppcbas  16991  rescbas  17102  rescco  17105  cofuass  17162  fucbas  17233  fuchom  17234  setccatid  17347  estrccatid  17385  xpcbas  17431  oduleval  17744  oduglb  17752  odulub  17754  ipotset  17770  efmndbas  18039  efmndbasabf  18040  symggrplem  18052  smndex1mndlem  18077  pwmnd  18105  grpinvfvi  18149  cntrval  18452  cntzval  18454  oppgplusfval  18479  snsymgefmndeq  18526  symgvalstruct  18528  pmtrprfval  18618  m1expaddsub  18629  sylow1lem2  18727  sylow3lem1  18755  oppglsm  18770  gsumzsplit  19050  gsum2dlem2  19094  gsumcom2  19098  dprd2dlem2  19165  dprd2da  19167  dmdprdsplit2lem  19170  mgpplusg  19246  mgpress  19253  ringidval  19256  opprmulfval  19378  abvtrivd  19614  sralem  19952  srasca  19956  sravsca  19957  sraip  19958  rlmval  19966  psrmulr  20167  mplmonmul  20248  mplcoe3  20250  opsrbaslem  20261  opsrtoslem2  20268  psr1val  20357  ply1basfvi  20412  ply1plusgfvi  20413  psr1sca2  20422  evl1fval1lem  20496  zlmlem  20667  zlmsca  20671  zlmvsca  20672  psgninv  20729  ocvval  20814  thlbas  20843  thlle  20844  thloc  20846  dsmmval2  20883  mattpos1  21068  mdettpos  21223  smadiadetglem1  21283  tgdif0  21603  indislem  21611  restco  21775  txtopon  22202  txindislem  22244  qtopres  22309  hmphindis  22408  ptuncnv  22418  snclseqg  22727  tsmssplit  22763  ussval  22871  tuslem  22879  setsmsbas  23088  tnglem  23252  tngds  23260  tngtset  23261  pcoass  23631  cphsqrtcl2  23793  rrxcph  23998  ovolunlem1a  24100  ioorinv  24180  itg11  24295  itg1mulc  24308  itg2cnlem1  24365  iblss2  24409  ibladdlem  24423  itgfsum  24430  iblabslem  24431  iblabs  24432  ditgneg  24458  deg1fvi  24682  dgrco  24868  logfac  25187  cxpexp  25254  cxpmul2  25275  cxpsqrt  25289  cxpsqrtth  25315  dvcxp1  25324  dvcxp2  25325  ang180lem1  25390  mcubic  25428  quart1  25437  reasinsin  25477  atanlogaddlem  25494  atantayl2  25519  log2tlbnd  25526  basellem2  25662  basellem3  25663  basellem5  25665  basellem8  25668  dchrmulid2  25831  bcp1ctr  25858  lgsneg  25900  lgsneg1  25901  lgsdir2  25909  lgsdir  25911  lgsdi  25913  lgsquad2lem2  25964  pntleml  26190  motgrp  26332  lmiisolem  26585  ttglem  26665  egrsubgr  27062  iswwlksnon  27634  iswspthsnon  27637  bafval  28384  ipidsq  28490  ipasslem1  28611  pjclem2  29976  cvmdi  30104  imadifxp  30354  iundisjcnt  30524  dpfrac1  30572  cycpmco2rn  30771  cyc3genpmlem  30797  resvsca  30907  indval2  31277  bayesth  31701  ofcccat  31817  plymulx  31822  subfacp1lem6  32436  satfdm  32620  mvtval  32751  mexval  32753  mexval2  32754  mdvval  32755  mrsubfval  32759  mrsubvrs  32773  msubfval  32775  elmsubrn  32779  mvhfval  32784  mpstval  32786  msrfval  32788  mstaval  32795  mthmval  32826  bccolsum  32975  dfrdg2  33044  dfrdg3  33045  frrlem12  33138  dfrdg4  33416  ordtoplem  33787  ordcmp  33799  curunc  34878  matunitlindflem2  34893  poimirlem6  34902  poimirlem7  34903  poimirlem11  34907  poimirlem12  34908  poimirlem13  34909  poimirlem14  34910  poimirlem16  34912  poimirlem19  34915  poimirlem21  34917  poimirlem22  34918  poimirlem27  34923  poimirlem31  34927  poimirlem32  34928  itg2addnclem2  34948  ibladdnclem  34952  iblabsnclem  34959  iblabsnc  34960  iblmulc2nc  34961  ftc1anclem8  34978  pmodN  36990  tgrpgrplem  37889  tendoplass  37923  tendoicl  37936  erngdvlem3  38130  dvhvaddass  38237  dib0  38304  dib1dim2  38308  diclspsn  38334  cdlemn8  38344  dihopelvalcpre  38388  djhcom  38545  nn0expgcd  39190  kelac2  39671  mendbas  39790  mendsca  39795  mendring  39798  iscard4  39906  relexp01min  40064  relexpaddss  40069  iotain  40755  addrcom  40813  rnsnf  41450  itgsinexplem1  42245  volioc  42263  dirkertrigeqlem1  42390  fourierdlem104  42502  sqwvfoura  42520  sqwvfourb  42521  fzopredsuc  43530  fppr2odd  43903  rngccatidALTV  44267  ringccatidALTV  44330  0dig2pr01  44677  nn0sumshdiglemB  44687