Theorem 3eqtr2d 2779

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3eqtr2d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr2d.2	⊢ (𝜑 → 𝐶 = 𝐵)
3eqtr2d.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
3eqtr2d	⊢ (𝜑 → 𝐴 = 𝐷)

Proof of Theorem 3eqtr2d

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtr2d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	1, 2	eqtr4d 2776	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtrd 2773	1 ⊢ (𝜑 → 𝐴 = 𝐷)

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  fmptapd  7166  negsub  11505  neg2sub  11517  divmuleq  11916  divneg2  11935  discr  14200  bcpasc  14278  hashgval2  14335  hashf1lem2  14414  relexpaddnn  14995  crim  15059  remullem  15072  isum1p  15784  geo2sum  15816  fallfacfwd  15977  fsumkthpow  15997  bpoly3  15999  bpoly4  16000  efi4p  16077  sinhval  16094  addcos  16114  cos2tsin  16119  demoivreALT  16141  rpnnen2lem11  16164  omeo  16306  pwp1fsum  16331  sadaddlem  16404  bitsres  16411  smumullem  16430  sqgcd  16499  eulerthlem2  16712  vfermltlALT  16732  pockthlem  16835  4sqlem10  16877  vdwlem2  16912  vdwlem6  16916  vdwlem8  16918  fuccocl  17914  resssetc  18039  resscatc  18056  uncfcurf  18189  yonedalem3b  18229  prdspjmhm  18707  grpinvid2  18874  imasgrp2  18935  mulgaddcomlem  18972  mulgmodid  18988  lagsubg2  19066  cntzsgrpcl  19193  cntzsubm  19197  sylow3lem2  19491  efgredleme  19606  ablsubsub  19680  ablsubsub4  19681  odadd2  19712  gex2abl  19714  pgpfac1lem3a  19941  pwspjmhmmgpd  20135  abvneg  20435  lmodfopne  20503  lsppr  20697  gzrngunit  21004  frlmsubgval  21312  frlmgsum  21319  psrass1  21517  resspsradd  21528  resspsrvsca  21530  mplcoe5  21587  mplmon2mul  21622  evlslem2  21634  evlsvarsrng  21654  coe1tm  21787  ply1scl1OLD  21808  evls1varsrng  21851  mamuass  21894  mavmulass  22043  mulmarep1gsum2  22068  mdetuni0  22115  maducoeval2  22134  madulid  22139  mat2pmatmul  22225  decpmatmulsumfsupp  22267  pmatcollpwlem  22274  pm2mpmhmlem1  22312  cmpfi  22904  cnconn  22918  txrest  23127  utopsnneiplem  23744  blcvx  24306  tcphcphlem2  24745  cphipval2  24750  cphipval  24752  rrx0  24906  minveclem2  24935  pjthlem1  24946  uniioovol  25088  uniioombllem2  25092  itg1addlem4  25208  itg1addlem4OLD  25209  mbfi1fseqlem5  25229  itg2mulc  25257  itg2monolem1  25260  itgaddlem1  25332  itgmulc2lem2  25342  dvrec  25464  lhop2  25524  ftc1lem5  25549  deg1submon1p  25662  plypf1  25718  coefv0  25754  coemulhi  25760  coemulc  25761  dgreq0  25771  dvply1  25789  vieta1  25817  aareccl  25831  aaliou3lem8  25850  dvtaylp  25874  mtest  25908  sineq0  26025  efif1olem2  26044  efif1olem4  26046  tanarg  26119  logtayl2  26162  nnlogbexp  26276  isosctrlem2  26314  chordthmlem2  26328  chordthmlem4  26330  heron  26333  dcubic1lem  26338  dcubic1  26340  mcubic  26342  dquart  26348  quart1lem  26350  quart1  26351  efiasin  26383  asinsin  26387  atancj  26405  efiatan  26407  atanlogaddlem  26408  cosatan  26416  atantan  26418  atans2  26426  log2cnv  26439  log2tlbnd  26440  birthdaylem2  26447  cxplim  26466  lgamgulmlem2  26524  wilthlem1  26562  basellem3  26577  musum  26685  musumsum  26686  muinv  26687  pclogsum  26708  mersenne  26720  dchrabs  26753  dchrinv  26754  lgseisenlem1  26868  lgsquadlem1  26873  lgsquadlem2  26874  lgsquadlem3  26875  lgsquad2lem1  26877  2lgslem1  26887  2sqmod  26929  chebbnd1lem3  26964  chpchtlim  26972  rplogsumlem2  26978  dchrisumlem2  26983  dchrmusum2  26987  mulog2sumlem1  27027  mulog2sumlem3  27029  vmalogdivsum2  27031  selberg4lem1  27053  pntrlog2bndlem2  27071  pntrlog2bndlem4  27073  pntibndlem2  27084  pntlemr  27095  pntlemf  27098  pntlemo  27100  addsdilem4  27599  ragcom  27939  colperpexlem1  27971  lmiisolem  28037  hypcgrlem2  28041  trgcopyeulem  28046  brbtwn2  28153  colinearalglem1  28154  colinearalglem2  28155  axcontlem2  28213  axcontlem8  28219  numedglnl  28394  clwlkclwwlklem2a  29241  numclwlk1lem1  29612  numclwlk1lem2  29613  numclwwlk2  29624  grpoinvid2  29770  ablodivdiv4  29795  smcnlem  29938  ipidsq  29951  ipasslem2  30073  minvecolem2  30116  hv2times  30302  pjhthlem1  30632  pjds3i  30954  ho2times  31060  opsqrlem6  31386  pjclem4  31440  pj3si  31448  csmdsymi  31575  ofoprabco  31877  fcnvgreu  31886  swrdrndisj  32109  trsp2cyc  32270  cycpmco2lem3  32275  cycpmco2lem4  32276  cycpmco2lem5  32277  cycpmco2lem6  32278  cycpmco2  32280  imaslmod  32457  ply1fermltlchr  32651  frlmdim  32685  rrxdim  32688  lbsdiflsp0  32700  fedgmullem1  32703  fedgmullem2  32704  extdg1id  32731  ccfldextdgrr  32735  qqhcn  32960  esumpr2  33054  esumpfinval  33062  esumpfinvalf  33063  carsggect  33306  oddpwdcv  33343  eulerpartlemgs2  33368  fibp1  33389  orvcelval  33456  ballotlemscr  33506  ballotlemfrci  33515  signsplypnf  33550  reprpmtf1o  33627  breprexplemc  33633  breprexp  33634  circlemeth  33641  lpadright  33685  revwlk  34104  subfacp1lem5  34164  cvmliftlem10  34274  circum  34648  faclimlem3  34704  fwddifnp1  35126  bj-bary1lem  36180  tan2h  36469  poimirlem3  36480  poimirlem13  36490  poimirlem14  36491  itgaddnclem1  36535  itgmulc2nclem2  36544  areacirclem1  36565  areacirclem4  36568  istotbnd3  36628  iscringd  36855  3atlem1  38343  pmod2iN  38709  polval2N  38766  lhple  38902  cdleme2  39088  cdleme35d  39312  cdleme42h  39342  cdlemeg46ngfr  39378  cdlemkid1  39782  lcfl7lem  40359  mapdpglem22  40553  mapdh6dN  40599  hdmap1l6d  40673  hdmapinvlem3  40780  lcmineqlem3  40885  selvvvval  41155  evlselv  41157  evlsmhpvvval  41165  nnadddir  41182  expgcd  41221  readdsub  41254  sn-negex12  41286  zmulcomlem  41325  prjspeclsp  41351  prjspner1  41365  3cubeslem3r  41411  diophin  41496  irrapxlem2  41547  pellexlem6  41558  pell1234qrmulcl  41579  rmxyval  41640  rmxyneg  41645  rmxyadd  41646  jm2.24  41688  jm2.25  41724  limexissupab  42019  omabs2  42068  tfsconcatrev  42084  naddwordnexlem4  42138  snhesn  42523  scottrankd  42993  radcnvrat  43059  binomcxplemnotnn0  43101  sub2times  43969  mul13d  43976  fperiodmullem  44000  fperiodmul  44001  isumneg  44305  climneg  44313  itgsinexp  44658  stoweidlem13  44716  stoweidlem42  44745  wallispilem4  44771  wallispilem5  44772  wallispi2lem1  44774  stirlinglem1  44777  stirlinglem3  44779  stirlinglem4  44780  stirlinglem5  44781  stirlinglem7  44783  stirlinglem10  44786  dirkertrigeqlem3  44803  fourierdlem30  44840  fourierdlem32  44842  fourierdlem42  44852  fourierdlem48  44857  fourierdlem49  44858  fourierdlem83  44892  sqwvfoura  44931  sqwvfourb  44932  etransclem2  44939  etransclem46  44983  sharhght  45568  imasetpreimafvbijlemfv  46057  fmtnorec3  46203  quad1  46275  requad1  46277  isomgreqve  46480  ushrisomgr  46496  rngcid  46831  ringcid  46877  lmodvsmdi  47012  dmatALTbas  47036  ldepsprlem  47107  itcovalt2lem2lem2  47314  ackval3  47323  1subrec1sub  47345  eenglngeehlnmlem1  47377  eenglngeehlnmlem2  47378  itsclc0xyqsolr  47409  sinhpcosh  47739