Theorem 3eqtr2d 2650

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

Syntax hints:   → wi 4   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  fmptapd  6342  negsub  10208  neg2sub  10220  divmuleq  10609  divneg2  10628  discr  12863  bcpasc  12970  hashgval2  13028  hashf1lem2  13097  relexpaddnn  13639  crim  13703  remullem  13716  isum1p  14412  geo2sum  14443  fallfacfwd  14606  fsumkthpow  14626  bpoly3  14628  bpoly4  14629  efi4p  14706  sinhval  14723  addcos  14743  cos2tsin  14748  demoivreALT  14770  rpnnen2lem11  14792  omeo  14928  pwp1fsum  14952  sadaddlem  15026  bitsres  15033  smumullem  15052  sqgcd  15116  eulerthlem2  15325  vfermltlALT  15345  pockthlem  15447  4sqlem10  15489  vdwlem2  15524  vdwlem6  15528  vdwlem8  15530  fuccocl  16447  resssetc  16565  resscatc  16578  uncfcurf  16702  yonedalem3b  16742  prdspjmhm  17190  grpinvid2  17294  imasgrp2  17353  mulgaddcomlem  17386  mulgmodid  17404  lagsubg2  17478  cntzsubm  17591  sylow3lem2  17866  efgredleme  17979  ablsubsub  18046  ablsubsub4  18047  odadd2  18075  gex2abl  18077  pgpfac1lem3a  18298  abvneg  18657  lmodfopne  18724  lsppr  18914  psrass1  19226  resspsradd  19237  resspsrvsca  19239  mplcoe5  19289  mplmon2mul  19322  evlslem2  19333  evlsvarsrng  19349  coe1tm  19464  ply1scl1  19483  evls1varsrng  19525  gzrngunit  19631  frlmsubgval  19927  frlmgsum  19930  mamuass  20027  mavmulass  20174  mulmarep1gsum2  20199  mdetuni0  20246  maducoeval2  20265  madulid  20270  mat2pmatmul  20355  decpmatmulsumfsupp  20397  pmatcollpwlem  20404  pm2mpmhmlem1  20442  cmpfi  21021  cnconn  21035  txrest  21244  utopsnneiplem  21861  blcvx  22409  tchcphlem2  22843  cphipval2  22848  cphipval  22850  minveclem2  23005  pjthlem1  23016  uniioovol  23153  uniioombllem2  23157  itg1addlem4  23272  mbfi1fseqlem5  23292  itg2mulc  23320  itg2monolem1  23323  itgaddlem1  23395  itgmulc2lem2  23405  dvrec  23524  lhop2  23582  ftc1lem5  23607  deg1submon1p  23716  plypf1  23772  coefv0  23808  coemulhi  23814  coemulc  23815  dgreq0  23825  dvply1  23843  vieta1  23871  aareccl  23885  aaliou3lem8  23904  dvtaylp  23928  mtest  23962  sineq0  24077  efif1olem2  24093  efif1olem4  24095  tanarg  24169  logtayl2  24208  nnlogbexp  24319  isosctrlem2  24349  chordthmlem2  24360  chordthmlem4  24362  heron  24365  dcubic1lem  24370  dcubic1  24372  mcubic  24374  dquart  24380  quart1lem  24382  quart1  24383  efiasin  24415  asinsin  24419  atancj  24437  efiatan  24439  atanlogaddlem  24440  cosatan  24448  atantan  24450  atans2  24458  log2cnv  24471  log2tlbnd  24472  birthdaylem2  24479  cxplim  24498  lgamgulmlem2  24556  wilthlem1  24594  basellem3  24609  musum  24717  musumsum  24718  muinv  24719  pclogsum  24740  mersenne  24752  dchrabs  24785  dchrinv  24786  lgseisenlem1  24900  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  lgsquad2lem1  24909  2lgslem1  24919  chebbnd1lem3  24960  chpchtlim  24968  rplogsumlem2  24974  dchrisumlem2  24979  dchrmusum2  24983  mulog2sumlem1  25023  mulog2sumlem3  25025  vmalogdivsum2  25027  selberg4lem1  25049  pntrlog2bndlem2  25067  pntrlog2bndlem4  25069  pntibndlem2  25080  pntlemr  25091  pntlemf  25094  pntlemo  25096  ragcom  25393  colperpexlem1  25422  lmiisolem  25488  hypcgrlem2  25492  trgcopyeulem  25497  brbtwn2  25585  colinearalglem1  25586  colinearalglem2  25587  axcontlem2  25645  axcontlem8  25651  basvtxval  25693  clwlkisclwwlklem2a  26313  numclwwlk2  26634  grpoinvid2  26767  ablodivdiv4  26792  smcnlem  26936  ipidsq  26949  ipasslem2  27071  minvecolem2  27115  hv2times  27302  pjhthlem1  27634  pjds3i  27956  ho2times  28062  opsqrlem6  28388  pjclem4  28442  pj3si  28450  csmdsymi  28577  ofoprabco  28847  fcnvgreu  28855  2sqmod  28979  qqhcn  29363  esumpr2  29456  esumpfinval  29464  esumpfinvalf  29465  carsggect  29707  oddpwdcv  29744  eulerpartlemgs2  29769  fibp1  29790  orvcelval  29857  ballotlemscr  29907  ballotlemfrci  29916  signsplypnf  29953  subfacp1lem5  30420  cvmliftlem10  30530  circum  30822  faclimlem3  30884  fwddifnp1  31442  bj-bary1lem  32337  tan2h  32571  poimirlem3  32582  poimirlem13  32592  poimirlem14  32593  itgaddnclem1  32638  itgmulc2nclem2  32647  areacirclem1  32670  areacirclem4  32673  istotbnd3  32740  iscringd  32967  3atlem1  33787  pmod2iN  34153  polval2N  34210  lhple  34346  cdleme2  34533  cdleme35d  34758  cdleme42h  34788  cdlemeg46ngfr  34824  cdlemkid1  35228  lcfl7lem  35806  mapdpglem22  36000  mapdh6dN  36046  hdmap1l6d  36121  hdmapinvlem3  36230  diophin  36354  irrapxlem2  36405  pellexlem6  36416  pell1234qrmulcl  36437  rmxyval  36498  rmxyneg  36503  rmxyadd  36504  jm2.24  36548  jm2.25  36584  snhesn  37100  radcnvrat  37535  binomcxplemnotnn0  37577  sub2times  38426  mul13d  38432  fperiodmullem  38458  fperiodmul  38459  isumneg  38669  climneg  38677  itgsinexp  38846  stoweidlem13  38906  stoweidlem42  38935  wallispilem4  38961  wallispilem5  38962  wallispi2lem1  38964  stirlinglem1  38967  stirlinglem3  38969  stirlinglem4  38970  stirlinglem5  38971  stirlinglem7  38973  stirlinglem10  38976  dirkertrigeqlem3  38993  fourierdlem30  39030  fourierdlem32  39032  fourierdlem42  39042  fourierdlem48  39047  fourierdlem49  39048  fourierdlem83  39082  sqwvfoura  39121  sqwvfourb  39122  etransclem2  39129  etransclem46  39173  sharhght  39703  fmtnorec3  39998  clwlkclwwlklem2a  41207  av-numclwwlk2  41537  rngcid  41771  ringcid  41817  lmodvsmdi  41957  dmatALTbas  41984  ldepsprlem  42055  sinhpcosh  42280