Theorem 3eqtr2d 2810

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

Syntax hints:   → wi 4   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  fmptapd  7167  scottrankd  9870  negsub  11502  neg2sub  11514  divmuleq  11916  divneg2  11935  nnadddir  12288  discr  14272  bcpasc  14353  hashgval2  14410  hashf1lem2  14489  relexpaddnn  15084  crim  15162  remullem  15175  isum1p  15891  geo2sum  15923  fallfacfwd  16086  fsumkthpow  16106  bpoly3  16108  bpoly4  16109  efi4p  16189  sinhval  16206  addcos  16226  cos2tsin  16231  demoivreALT  16253  rpnnen2lem11  16276  omeo  16420  pwp1fsum  16445  sadaddlem  16520  bitsres  16527  smumullem  16546  sqgcd  16616  expgcd  16617  eulerthlem2  16837  vfermltlALT  16858  pockthlem  16961  4sqlem10  17003  vdwlem2  17038  vdwlem6  17042  vdwlem8  17044  fuccocl  18020  resssetc  18145  resscatc  18162  uncfcurf  18291  yonedalem3b  18331  prdspjmhm  18884  grpinvid2  19055  imasgrp2  19117  mulgaddcomlem  19159  mulgmodid  19175  lagsubg2  19261  cntzsgrpcl  19400  cntzsubm  19404  sylow3lem2  19694  efgredleme  19809  ablsubsub  19883  ablsubsub4  19884  odadd2  19915  gex2abl  19917  pgpfac1lem3a  20144  pwspjmhmmgpd  20405  rngcid  20716  ringcid  20745  abvneg  20903  lmodfopne  20995  lsppr  21188  rngqiprngfulem4  21421  gzrngunit  21548  frlmsubgval  21880  frlmgsum  21887  psrass1  22078  resspsradd  22089  resspsrvsca  22091  mplcoe5  22156  mplmon2mul  22185  evlslem2  22195  evlsvarsrng  22223  selvvvval  22258  coe1tm  22399  ply1fermltlchr  22437  evls1varsrng  22465  mamuass  22524  mavmulass  22671  mulmarep1gsum2  22696  mdetuni0  22743  maducoeval2  22762  madulid  22767  mat2pmatmul  22853  decpmatmulsumfsupp  22895  pmatcollpwlem  22902  pm2mpmhmlem1  22940  cmpfi  23530  cnconn  23544  txrest  23753  utopsnneiplem  24369  blcvx  24920  tcphcphlem2  25360  cphipval2  25365  cphipval  25367  rrx0  25521  minveclem2  25550  pjthlem1  25561  uniioovol  25703  uniioombllem2  25707  itg1addlem4  25823  mbfi1fseqlem5  25843  itg2mulc  25871  itg2monolem1  25874  itgaddlem1  25947  itgmulc2lem2  25957  dvrec  26079  lhop2  26139  ftc1lem5  26164  deg1submon1p  26275  plypf1  26334  coefv0  26370  coemulhi  26376  coemulc  26377  dgreq0  26387  dvply1  26410  vieta1  26438  aareccl  26452  aaliou3lem8  26471  dvtaylp  26495  mtest  26529  sineq0  26651  efif1olem2  26670  efif1olem4  26672  tanarg  26746  logtayl2  26789  nnlogbexp  26908  isosctrlem2  26946  chordthmlem2  26960  chordthmlem4  26962  heron  26965  dcubic1lem  26970  dcubic1  26972  mcubic  26974  dquart  26980  quart1lem  26982  quart1  26983  efiasin  27015  asinsin  27019  atancj  27037  efiatan  27039  atanlogaddlem  27040  cosatan  27048  atantan  27050  atans2  27058  log2cnv  27071  log2tlbnd  27072  birthdaylem2  27079  cxplim  27098  lgamgulmlem2  27156  wilthlem1  27194  basellem3  27209  musum  27317  musumsum  27318  muinv  27319  pclogsum  27341  mersenne  27353  dchrabs  27386  dchrinv  27387  lgseisenlem1  27501  lgsquadlem1  27506  lgsquadlem2  27507  lgsquadlem3  27508  lgsquad2lem1  27510  2lgslem1  27520  2sqmod  27562  chebbnd1lem3  27597  chpchtlim  27605  rplogsumlem2  27611  dchrisumlem2  27616  dchrmusum2  27620  mulog2sumlem1  27660  mulog2sumlem3  27662  vmalogdivsum2  27664  selberg4lem1  27686  pntrlog2bndlem2  27704  pntrlog2bndlem4  27706  pntibndlem2  27717  pntlemr  27728  pntlemf  27731  pntlemo  27733  addsdilem4  28309  mulsunif2lem  28324  halfcut  28613  bdayfinbndlem1  28622  ragcom  28933  colperpexlem1  28966  plngrotlem2  29024  plng3p  29033  lmiisolem  29059  hypcgrlem2  29063  trgcopyeulem  29069  brbtwn2  29192  colinearalglem1  29193  colinearalglem2  29194  axcontlem2  29252  axcontlem8  29258  numedglnl  29431  clwlkclwwlklem2a  30286  numclwlk1lem1  30657  numclwlk1lem2  30658  numclwwlk2  30669  grpoinvid2  30818  ablodivdiv4  30843  smcnlem  30986  ipidsq  30999  ipasslem2  31121  minvecolem2  31164  hv2times  31350  pjhthlem1  31680  pjds3i  32002  ho2times  32108  opsqrlem6  32434  pjclem4  32488  pj3si  32496  csmdsymi  32623  ofoprabco  32946  fcnvgreu  32954  quad3d  33031  nn0diffz0  33076  swrdrndisj  33214  trsp2cyc  33380  cycpmco2lem3  33385  cycpmco2lem4  33386  cycpmco2lem5  33387  cycpmco2lem6  33388  cycpmco2  33390  conjga  33427  elrgspnlem1  33499  rlocmulval  33527  rlocinvunit  33532  rlocisunit  33533  imaslmod  33612  1arithufdlem3  33777  deg1prod  33814  r1padd1  33839  selvply1rhmlem2  33852  mplvrpmrhm  33878  esplyfvaln  33905  frlmdim  33942  rrxdim  33945  lbsdiflsp0  33957  fedgmullem1  33960  fedgmullem2  33961  extdg1id  33997  ccfldextdgrr  34003  fldextrspunlem1  34006  constrrtlc1  34063  constrrtcclem  34065  constrrtcc  34066  constrrecl  34100  constrresqrtcl  34108  cos9thpiminplylem1  34113  cos9thpiminplylem2  34114  cos9thpiminplylem3  34115  cos9thpiminply  34119  qqhcn  34322  esumpr2  34398  esumpfinval  34406  esumpfinvalf  34407  carsggect  34649  oddpwdcv  34686  eulerpartlemgs2  34711  fibp1  34732  orvcelval  34800  ballotlemscr  34850  ballotlemfrci  34859  signsplypnf  34878  reprpmtf1o  34954  breprexplemc  34960  breprexp  34961  circlemeth  34968  lpadright  35015  revwlk  35512  subfacp1lem5  35571  cvmliftlem10  35681  circum  36061  faclimlem3  36132  fwddifnp1  36552  bj-bary1lem  37837  qdiff  37854  tan2h  38146  poimirlem3  38157  poimirlem13  38167  poimirlem14  38168  itgaddnclem1  38212  itgmulc2nclem2  38221  areacirclem1  38242  areacirclem4  38245  istotbnd3  38305  iscringd  38532  3atlem1  40142  pmod2iN  40508  polval2N  40565  lhple  40701  cdleme2  40887  cdleme35d  41111  cdleme42h  41141  cdlemeg46ngfr  41177  cdlemkid1  41581  lcfl7lem  42158  mapdpglem22  42352  mapdh6dN  42398  hdmap1l6d  42472  hdmapinvlem3  42579  lcmineqlem3  42683  readvrec2  43005  readdsub  43028  sn-negex12  43061  zmulcomlem  43124  evlselv  43206  evlsmhpvvval  43212  prjspeclsp  43229  prjspner1  43243  3cubeslem3r  43303  diophin  43388  irrapxlem2  43435  pellexlem6  43446  pell1234qrmulcl  43467  rmxyval  43527  rmxyneg  43532  rmxyadd  43533  jm2.24  43575  jm2.25  43611  limexissupab  43895  omabs2  43944  tfsconcatrev  43960  naddwordnexlem4  44013  snhesn  44397  radcnvrat  44909  binomcxplemnotnn0  44951  sub2times  45877  mul13d  45884  fperiodmullem  45907  fperiodmul  45908  isumneg  46203  climneg  46211  itgsinexp  46554  stoweidlem13  46612  stoweidlem42  46641  wallispilem4  46667  wallispilem5  46668  wallispi2lem1  46670  stirlinglem1  46673  stirlinglem3  46675  stirlinglem4  46676  stirlinglem5  46677  stirlinglem7  46679  stirlinglem10  46682  dirkertrigeqlem3  46699  fourierdlem30  46736  fourierdlem32  46738  fourierdlem42  46748  fourierdlem48  46753  fourierdlem49  46754  fourierdlem83  46788  sqwvfoura  46827  sqwvfourb  46828  etransclem2  46835  etransclem46  46879  sharhght  47464  sin3t  47490  sin5tlem1  47492  sin5tlem3  47494  cos5t  47498  imasetpreimafvbijlemfv  48033  fmtnorec3  48182  quad1  48267  requad1  48269  ushggricedg  48574  lmodvsmdi  49037  dmatALTbas  49059  ldepsprlem  49130  itcovalt2lem2lem2  49332  ackval3  49341  1subrec1sub  49363  eenglngeehlnmlem1  49395  eenglngeehlnmlem2  49396  itsclc0xyqsolr  49427  swapfid  49935  sinhpcosh  50396