Theorem 3eqtr2d 2806

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 2803	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtrd 2800	1 ⊢ (𝜑 → 𝐴 = 𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  fmptapd  7173  scottrankd  9881  negsub  11517  neg2sub  11529  divmuleq  11931  divneg2  11950  nnadddir  12303  discr  14289  bcpasc  14370  hashgval2  14427  hashf1lem2  14506  relexpaddnn  15107  crim  15185  remullem  15198  isum1p  15913  geo2sum  15945  fallfacfwd  16107  fsumkthpow  16127  bpoly3  16129  bpoly4  16130  efi4p  16210  sinhval  16227  addcos  16247  cos2tsin  16252  demoivreALT  16274  rpnnen2lem11  16297  omeo  16441  pwp1fsum  16466  sadaddlem  16541  bitsres  16548  smumullem  16567  sqgcd  16637  expgcd  16638  eulerthlem2  16858  vfermltlALT  16879  pockthlem  16982  4sqlem10  17024  vdwlem2  17059  vdwlem6  17063  vdwlem8  17065  fuccocl  18041  resssetc  18166  resscatc  18183  uncfcurf  18312  yonedalem3b  18352  prdspjmhm  18911  grpinvid2  19082  imasgrp2  19144  mulgaddcomlem  19186  mulgmodid  19202  lagsubg2  19288  cntzsgrpcl  19427  cntzsubm  19431  sylow3lem2  19721  efgredleme  19836  ablsubsub  19910  ablsubsub4  19911  odadd2  19942  gex2abl  19944  pgpfac1lem3a  20171  pwspjmhmmgpd  20434  rngcid  20763  ringcid  20792  abvneg  20958  lmodfopne  21050  lsppr  21243  rngqiprngfulem4  21483  gzrngunit  21612  frlmsubgval  21944  frlmgsum  21951  psrass1  22142  resspsradd  22153  resspsrvsca  22155  mplcoe5  22220  mplmon2mul  22249  evlslem2  22259  evlsvarsrng  22287  selvvvval  22322  coe1tm  22463  ply1fermltlchr  22501  evls1varsrng  22529  mamuass  22588  mavmulass  22735  mulmarep1gsum2  22760  mdetuni0  22807  maducoeval2  22826  madulid  22831  mat2pmatmul  22917  decpmatmulsumfsupp  22959  pmatcollpwlem  22966  pm2mpmhmlem1  23004  cmpfi  23594  cnconn  23608  txrest  23817  utopsnneiplem  24433  blcvx  24984  tcphcphlem2  25424  cphipval2  25429  cphipval  25431  rrx0  25585  minveclem2  25614  pjthlem1  25625  uniioovol  25767  uniioombllem2  25771  itg1addlem4  25887  mbfi1fseqlem5  25907  itg2mulc  25935  itg2monolem1  25938  itgaddlem1  26011  itgmulc2lem2  26021  dvrec  26143  lhop2  26203  ftc1lem5  26228  deg1submon1p  26339  plypf1  26398  coefv0  26434  coemulhi  26440  coemulc  26441  dgreq0  26451  dvply1  26474  vieta1  26502  aareccl  26518  aaliou3lem8  26537  dvtaylp  26562  mtest  26596  sineq0  26718  efif1olem2  26737  efif1olem4  26739  tanarg  26813  logtayl2  26856  nnlogbexp  26975  isosctrlem2  27013  chordthmlem2  27027  chordthmlem4  27029  heron  27032  dcubic1lem  27037  dcubic1  27039  mcubic  27041  dquart  27047  quart1lem  27049  quart1  27050  efiasin  27082  asinsin  27086  atancj  27104  efiatan  27106  atanlogaddlem  27107  cosatan  27115  atantan  27117  atans2  27125  log2cnv  27138  log2tlbnd  27139  birthdaylem2  27146  cxplim  27165  lgamgulmlem2  27223  wilthlem1  27261  basellem3  27276  musum  27384  musumsum  27385  muinv  27386  pclogsum  27408  mersenne  27420  dchrabs  27453  dchrinv  27454  lgseisenlem1  27568  lgsquadlem1  27573  lgsquadlem2  27574  lgsquadlem3  27575  lgsquad2lem1  27577  2lgslem1  27587  2sqmod  27629  chebbnd1lem3  27664  chpchtlim  27672  rplogsumlem2  27678  dchrisumlem2  27683  dchrmusum2  27687  mulog2sumlem1  27727  mulog2sumlem3  27729  vmalogdivsum2  27731  selberg4lem1  27753  pntrlog2bndlem2  27771  pntrlog2bndlem4  27773  pntibndlem2  27784  pntlemr  27795  pntlemf  27798  pntlemo  27800  addsdilem4  28376  mulsunif2lem  28391  halfcut  28680  bdayfinbndlem1  28689  ragcom  29007  colperpexlem1  29040  plngrotlem2  29099  plng3p  29108  lmiisolem  29134  hypcgrlem2  29139  trgcopyeulem  29145  brbtwn2  29284  colinearalglem1  29285  colinearalglem2  29286  axcontlem2  29344  axcontlem8  29350  numedglnl  29523  clwlkclwwlklem2a  30378  numclwlk1lem1  30749  numclwlk1lem2  30750  numclwwlk2  30761  grpoinvid2  30910  ablodivdiv4  30935  smcnlem  31078  ipidsq  31091  ipasslem2  31213  minvecolem2  31256  hv2times  31442  pjhthlem1  31772  pjds3i  32094  ho2times  32200  opsqrlem6  32526  pjclem4  32580  pj3si  32588  csmdsymi  32715  ofoprabco  33038  fcnvgreu  33046  quad3d  33123  nn0diffz0  33168  swrdrndisj  33300  trsp2cyc  33466  cycpmco2lem3  33471  cycpmco2lem4  33472  cycpmco2lem5  33473  cycpmco2lem6  33474  cycpmco2  33476  conjga  33513  elrgspnlem1  33585  rlocmulval  33613  rlocinvunit  33618  rlocisunit  33619  imaslmod  33696  1arithufdlem3  33859  deg1prod  33896  r1padd1  33921  selvply1rhmlem2  33934  mplvrpmrhm  33960  esplyfvaln  33987  frlmdim  34024  rrxdim  34027  lbsdiflsp0  34039  fedgmullem1  34042  fedgmullem2  34043  extdg1id  34079  ccfldextdgrr  34085  fldextrspunlem1  34088  constrrtlc1  34145  constrrtcclem  34147  constrrtcc  34148  constrrecl  34182  constrresqrtcl  34190  cos9thpiminplylem1  34195  cos9thpiminplylem2  34196  cos9thpiminplylem3  34197  cos9thpiminply  34201  qqhcn  34404  esumpr2  34480  esumpfinval  34488  esumpfinvalf  34489  carsggect  34732  oddpwdcv  34769  eulerpartlemgs2  34794  fibp1  34815  orvcelval  34883  ballotlemscr  34933  ballotlemfrci  34942  signsplypnf  34961  reprpmtf1o  35037  breprexplemc  35043  breprexp  35044  circlemeth  35051  lpadright  35098  revwlk  35630  subfacp1lem5  35689  cvmliftlem10  35799  circum  36179  faclimlem3  36250  fwddifnp1  36670  bj-bary1lem  37987  qdiff  38004  tan2h  38296  poimirlem3  38307  poimirlem13  38317  poimirlem14  38318  itgaddnclem1  38362  itgmulc2nclem2  38371  areacirclem1  38392  areacirclem4  38395  istotbnd3  38455  iscringd  38682  3atlem1  40290  pmod2iN  40656  polval2N  40713  lhple  40849  cdleme2  41035  cdleme35d  41259  cdleme42h  41289  cdlemeg46ngfr  41325  cdlemkid1  41729  lcfl7lem  42306  mapdpglem22  42500  mapdh6dN  42546  hdmap1l6d  42620  hdmapinvlem3  42727  lcmineqlem3  42831  readvrec2  43155  readdsub  43178  sn-negex12  43211  zmulcomlem  43274  evlselv  43354  evlsmhpvvval  43360  prjspeclsp  43377  prjspner1  43391  3cubeslem3r  43451  diophin  43536  irrapxlem2  43583  pellexlem6  43594  pell1234qrmulcl  43615  rmxyval  43675  rmxyneg  43680  rmxyadd  43681  jm2.24  43723  jm2.25  43759  limexissupab  44043  omabs2  44092  tfsconcatrev  44108  naddwordnexlem4  44161  snhesn  44545  radcnvrat  45057  binomcxplemnotnn0  45099  sub2times  46025  mul13d  46032  fperiodmullem  46055  fperiodmul  46056  isumneg  46351  climneg  46359  itgsinexp  46702  stoweidlem13  46760  stoweidlem42  46789  wallispilem4  46815  wallispilem5  46816  wallispi2lem1  46818  stirlinglem1  46821  stirlinglem3  46823  stirlinglem4  46824  stirlinglem5  46825  stirlinglem7  46827  stirlinglem10  46830  dirkertrigeqlem3  46847  fourierdlem30  46884  fourierdlem32  46886  fourierdlem42  46896  fourierdlem48  46901  fourierdlem49  46902  fourierdlem83  46936  sqwvfoura  46975  sqwvfourb  46976  etransclem2  46983  etransclem46  47027  sharhght  47612  sin3t  47641  sin5tlem1  47643  sin5tlem3  47645  cos5t  47649  imasetpreimafvbijlemfv  48184  fmtnorec3  48333  quad1  48418  requad1  48420  ushggricedg  48725  lmodvsmdi  49192  dmatALTbas  49214  ldepsprlem  49285  itcovalt2lem2lem2  49487  ackval3  49496  1subrec1sub  49518  eenglngeehlnmlem1  49550  eenglngeehlnmlem2  49551  itsclc0xyqsolr  49582  swapfid  50090  sinhpcosh  50551