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  7170  scottrankd  9873  negsub  11505  neg2sub  11517  divmuleq  11919  divneg2  11938  nnadddir  12291  discr  14275  bcpasc  14356  hashgval2  14413  hashf1lem2  14492  relexpaddnn  15087  crim  15165  remullem  15178  isum1p  15894  geo2sum  15926  fallfacfwd  16089  fsumkthpow  16109  bpoly3  16111  bpoly4  16112  efi4p  16192  sinhval  16209  addcos  16229  cos2tsin  16234  demoivreALT  16256  rpnnen2lem11  16279  omeo  16423  pwp1fsum  16448  sadaddlem  16523  bitsres  16530  smumullem  16549  sqgcd  16619  expgcd  16620  eulerthlem2  16840  vfermltlALT  16861  pockthlem  16964  4sqlem10  17006  vdwlem2  17041  vdwlem6  17045  vdwlem8  17047  fuccocl  18023  resssetc  18148  resscatc  18165  uncfcurf  18294  yonedalem3b  18334  prdspjmhm  18887  grpinvid2  19058  imasgrp2  19120  mulgaddcomlem  19162  mulgmodid  19178  lagsubg2  19264  cntzsgrpcl  19403  cntzsubm  19407  sylow3lem2  19697  efgredleme  19812  ablsubsub  19886  ablsubsub4  19887  odadd2  19918  gex2abl  19920  pgpfac1lem3a  20147  pwspjmhmmgpd  20408  rngcid  20719  ringcid  20748  abvneg  20906  lmodfopne  20998  lsppr  21191  rngqiprngfulem4  21424  gzrngunit  21551  frlmsubgval  21883  frlmgsum  21890  psrass1  22081  resspsradd  22092  resspsrvsca  22094  mplcoe5  22159  mplmon2mul  22188  evlslem2  22198  evlsvarsrng  22226  selvvvval  22261  coe1tm  22402  ply1fermltlchr  22440  evls1varsrng  22468  mamuass  22527  mavmulass  22674  mulmarep1gsum2  22699  mdetuni0  22746  maducoeval2  22765  madulid  22770  mat2pmatmul  22856  decpmatmulsumfsupp  22898  pmatcollpwlem  22905  pm2mpmhmlem1  22943  cmpfi  23533  cnconn  23547  txrest  23756  utopsnneiplem  24372  blcvx  24923  tcphcphlem2  25363  cphipval2  25368  cphipval  25370  rrx0  25524  minveclem2  25553  pjthlem1  25564  uniioovol  25706  uniioombllem2  25710  itg1addlem4  25826  mbfi1fseqlem5  25846  itg2mulc  25874  itg2monolem1  25877  itgaddlem1  25950  itgmulc2lem2  25960  dvrec  26082  lhop2  26142  ftc1lem5  26167  deg1submon1p  26278  plypf1  26337  coefv0  26373  coemulhi  26379  coemulc  26380  dgreq0  26390  dvply1  26413  vieta1  26441  aareccl  26455  aaliou3lem8  26474  dvtaylp  26498  mtest  26532  sineq0  26654  efif1olem2  26673  efif1olem4  26675  tanarg  26749  logtayl2  26792  nnlogbexp  26911  isosctrlem2  26949  chordthmlem2  26963  chordthmlem4  26965  heron  26968  dcubic1lem  26973  dcubic1  26975  mcubic  26977  dquart  26983  quart1lem  26985  quart1  26986  efiasin  27018  asinsin  27022  atancj  27040  efiatan  27042  atanlogaddlem  27043  cosatan  27051  atantan  27053  atans2  27061  log2cnv  27074  log2tlbnd  27075  birthdaylem2  27082  cxplim  27101  lgamgulmlem2  27159  wilthlem1  27197  basellem3  27212  musum  27320  musumsum  27321  muinv  27322  pclogsum  27344  mersenne  27356  dchrabs  27389  dchrinv  27390  lgseisenlem1  27504  lgsquadlem1  27509  lgsquadlem2  27510  lgsquadlem3  27511  lgsquad2lem1  27513  2lgslem1  27523  2sqmod  27565  chebbnd1lem3  27600  chpchtlim  27608  rplogsumlem2  27614  dchrisumlem2  27619  dchrmusum2  27623  mulog2sumlem1  27663  mulog2sumlem3  27665  vmalogdivsum2  27667  selberg4lem1  27689  pntrlog2bndlem2  27707  pntrlog2bndlem4  27709  pntibndlem2  27720  pntlemr  27731  pntlemf  27734  pntlemo  27736  addsdilem4  28312  mulsunif2lem  28327  halfcut  28616  bdayfinbndlem1  28625  ragcom  28936  colperpexlem1  28969  plngrotlem2  29027  plng3p  29036  lmiisolem  29062  hypcgrlem2  29066  trgcopyeulem  29072  brbtwn2  29195  colinearalglem1  29196  colinearalglem2  29197  axcontlem2  29255  axcontlem8  29261  numedglnl  29434  clwlkclwwlklem2a  30289  numclwlk1lem1  30660  numclwlk1lem2  30661  numclwwlk2  30672  grpoinvid2  30821  ablodivdiv4  30846  smcnlem  30989  ipidsq  31002  ipasslem2  31124  minvecolem2  31167  hv2times  31353  pjhthlem1  31683  pjds3i  32005  ho2times  32111  opsqrlem6  32437  pjclem4  32491  pj3si  32499  csmdsymi  32626  ofoprabco  32949  fcnvgreu  32957  quad3d  33034  nn0diffz0  33079  swrdrndisj  33217  trsp2cyc  33383  cycpmco2lem3  33388  cycpmco2lem4  33389  cycpmco2lem5  33390  cycpmco2lem6  33391  cycpmco2  33393  conjga  33430  elrgspnlem1  33502  rlocmulval  33530  rlocinvunit  33535  rlocisunit  33536  imaslmod  33615  1arithufdlem3  33780  deg1prod  33817  r1padd1  33842  selvply1rhmlem2  33855  mplvrpmrhm  33881  esplyfvaln  33908  frlmdim  33945  rrxdim  33948  lbsdiflsp0  33960  fedgmullem1  33963  fedgmullem2  33964  extdg1id  34000  ccfldextdgrr  34006  fldextrspunlem1  34009  constrrtlc1  34066  constrrtcclem  34068  constrrtcc  34069  constrrecl  34103  constrresqrtcl  34111  cos9thpiminplylem1  34116  cos9thpiminplylem2  34117  cos9thpiminplylem3  34118  cos9thpiminply  34122  qqhcn  34325  esumpr2  34401  esumpfinval  34409  esumpfinvalf  34410  carsggect  34652  oddpwdcv  34689  eulerpartlemgs2  34714  fibp1  34735  orvcelval  34803  ballotlemscr  34853  ballotlemfrci  34862  signsplypnf  34881  reprpmtf1o  34957  breprexplemc  34963  breprexp  34964  circlemeth  34971  lpadright  35018  revwlk  35515  subfacp1lem5  35574  cvmliftlem10  35684  circum  36064  faclimlem3  36135  fwddifnp1  36555  bj-bary1lem  37841  qdiff  37858  tan2h  38150  poimirlem3  38161  poimirlem13  38171  poimirlem14  38172  itgaddnclem1  38216  itgmulc2nclem2  38225  areacirclem1  38246  areacirclem4  38249  istotbnd3  38309  iscringd  38536  3atlem1  40146  pmod2iN  40512  polval2N  40569  lhple  40705  cdleme2  40891  cdleme35d  41115  cdleme42h  41145  cdlemeg46ngfr  41181  cdlemkid1  41585  lcfl7lem  42162  mapdpglem22  42356  mapdh6dN  42402  hdmap1l6d  42476  hdmapinvlem3  42583  lcmineqlem3  42687  readvrec2  43011  readdsub  43034  sn-negex12  43067  zmulcomlem  43130  evlselv  43212  evlsmhpvvval  43218  prjspeclsp  43235  prjspner1  43249  3cubeslem3r  43309  diophin  43394  irrapxlem2  43441  pellexlem6  43452  pell1234qrmulcl  43473  rmxyval  43533  rmxyneg  43538  rmxyadd  43539  jm2.24  43581  jm2.25  43617  limexissupab  43901  omabs2  43950  tfsconcatrev  43966  naddwordnexlem4  44019  snhesn  44403  radcnvrat  44915  binomcxplemnotnn0  44957  sub2times  45883  mul13d  45890  fperiodmullem  45913  fperiodmul  45914  isumneg  46209  climneg  46217  itgsinexp  46560  stoweidlem13  46618  stoweidlem42  46647  wallispilem4  46673  wallispilem5  46674  wallispi2lem1  46676  stirlinglem1  46679  stirlinglem3  46681  stirlinglem4  46682  stirlinglem5  46683  stirlinglem7  46685  stirlinglem10  46688  dirkertrigeqlem3  46705  fourierdlem30  46742  fourierdlem32  46744  fourierdlem42  46754  fourierdlem48  46759  fourierdlem49  46760  fourierdlem83  46794  sqwvfoura  46833  sqwvfourb  46834  etransclem2  46841  etransclem46  46885  sharhght  47470  sin3t  47496  sin5tlem1  47498  sin5tlem3  47500  cos5t  47504  imasetpreimafvbijlemfv  48039  fmtnorec3  48188  quad1  48273  requad1  48275  ushggricedg  48580  lmodvsmdi  49043  dmatALTbas  49065  ldepsprlem  49136  itcovalt2lem2lem2  49338  ackval3  49347  1subrec1sub  49369  eenglngeehlnmlem1  49401  eenglngeehlnmlem2  49402  itsclc0xyqsolr  49433  swapfid  49941  sinhpcosh  50402