Theorem 3eqtr2d 2770

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  fmptapd  7111  negsub  11430  neg2sub  11442  divmuleq  11847  divneg2  11866  discr  14165  bcpasc  14246  hashgval2  14303  hashf1lem2  14381  relexpaddnn  14976  crim  15040  remullem  15053  isum1p  15766  geo2sum  15798  fallfacfwd  15961  fsumkthpow  15981  bpoly3  15983  bpoly4  15984  efi4p  16064  sinhval  16081  addcos  16101  cos2tsin  16106  demoivreALT  16128  rpnnen2lem11  16151  omeo  16295  pwp1fsum  16320  sadaddlem  16395  bitsres  16402  smumullem  16421  sqgcd  16491  expgcd  16492  eulerthlem2  16711  vfermltlALT  16732  pockthlem  16835  4sqlem10  16877  vdwlem2  16912  vdwlem6  16916  vdwlem8  16918  fuccocl  17892  resssetc  18017  resscatc  18034  uncfcurf  18163  yonedalem3b  18203  prdspjmhm  18721  grpinvid2  18889  imasgrp2  18952  mulgaddcomlem  18994  mulgmodid  19010  lagsubg2  19091  cntzsgrpcl  19231  cntzsubm  19235  sylow3lem2  19525  efgredleme  19640  ablsubsub  19714  ablsubsub4  19715  odadd2  19746  gex2abl  19748  pgpfac1lem3a  19975  pwspjmhmmgpd  20231  rngcid  20538  ringcid  20567  abvneg  20729  lmodfopne  20821  lsppr  21015  rngqiprngfulem4  21239  gzrngunit  21358  frlmsubgval  21690  frlmgsum  21697  psrass1  21889  resspsradd  21900  resspsrvsca  21902  mplcoe5  21963  mplmon2mul  21992  evlslem2  22002  evlsvarsrng  22022  coe1tm  22175  ply1scl1OLD  22196  ply1fermltlchr  22215  evls1varsrng  22243  mamuass  22305  mavmulass  22452  mulmarep1gsum2  22477  mdetuni0  22524  maducoeval2  22543  madulid  22548  mat2pmatmul  22634  decpmatmulsumfsupp  22676  pmatcollpwlem  22683  pm2mpmhmlem1  22721  cmpfi  23311  cnconn  23325  txrest  23534  utopsnneiplem  24151  blcvx  24702  tcphcphlem2  25152  cphipval2  25157  cphipval  25159  rrx0  25313  minveclem2  25342  pjthlem1  25353  uniioovol  25496  uniioombllem2  25500  itg1addlem4  25616  mbfi1fseqlem5  25636  itg2mulc  25664  itg2monolem1  25667  itgaddlem1  25740  itgmulc2lem2  25750  dvrec  25875  lhop2  25936  ftc1lem5  25963  deg1submon1p  26074  plypf1  26133  coefv0  26169  coemulhi  26175  coemulc  26176  dgreq0  26187  dvply1  26207  vieta1  26236  aareccl  26250  aaliou3lem8  26269  dvtaylp  26294  mtest  26329  sineq0  26449  efif1olem2  26468  efif1olem4  26470  tanarg  26544  logtayl2  26587  nnlogbexp  26707  isosctrlem2  26745  chordthmlem2  26759  chordthmlem4  26761  heron  26764  dcubic1lem  26769  dcubic1  26771  mcubic  26773  dquart  26779  quart1lem  26781  quart1  26782  efiasin  26814  asinsin  26818  atancj  26836  efiatan  26838  atanlogaddlem  26839  cosatan  26847  atantan  26849  atans2  26857  log2cnv  26870  log2tlbnd  26871  birthdaylem2  26878  cxplim  26898  lgamgulmlem2  26956  wilthlem1  26994  basellem3  27009  musum  27117  musumsum  27118  muinv  27119  pclogsum  27142  mersenne  27154  dchrabs  27187  dchrinv  27188  lgseisenlem1  27302  lgsquadlem1  27307  lgsquadlem2  27308  lgsquadlem3  27309  lgsquad2lem1  27311  2lgslem1  27321  2sqmod  27363  chebbnd1lem3  27398  chpchtlim  27406  rplogsumlem2  27412  dchrisumlem2  27417  dchrmusum2  27421  mulog2sumlem1  27461  mulog2sumlem3  27463  vmalogdivsum2  27465  selberg4lem1  27487  pntrlog2bndlem2  27505  pntrlog2bndlem4  27507  pntibndlem2  27518  pntlemr  27529  pntlemf  27532  pntlemo  27534  addsdilem4  28080  mulsunif2lem  28095  halfcut  28364  zs12bday  28379  ragcom  28661  colperpexlem1  28693  lmiisolem  28759  hypcgrlem2  28763  trgcopyeulem  28768  brbtwn2  28868  colinearalglem1  28869  colinearalglem2  28870  axcontlem2  28928  axcontlem8  28934  numedglnl  29107  clwlkclwwlklem2a  29960  numclwlk1lem1  30331  numclwlk1lem2  30332  numclwwlk2  30343  grpoinvid2  30491  ablodivdiv4  30516  smcnlem  30659  ipidsq  30672  ipasslem2  30794  minvecolem2  30837  hv2times  31023  pjhthlem1  31353  pjds3i  31675  ho2times  31781  opsqrlem6  32107  pjclem4  32161  pj3si  32169  csmdsymi  32296  ofoprabco  32621  fcnvgreu  32630  quad3d  32706  swrdrndisj  32912  trsp2cyc  33078  cycpmco2lem3  33083  cycpmco2lem4  33084  cycpmco2lem5  33085  cycpmco2lem6  33086  cycpmco2  33088  conjga  33125  elrgspnlem1  33195  rlocmulval  33222  imaslmod  33303  1arithufdlem3  33496  r1padd1  33552  frlmdim  33586  rrxdim  33589  lbsdiflsp0  33601  fedgmullem1  33604  fedgmullem2  33605  extdg1id  33640  ccfldextdgrr  33646  fldextrspunlem1  33649  constrrtlc1  33701  constrrtcclem  33703  constrrtcc  33704  constrrecl  33738  constrresqrtcl  33746  cos9thpiminplylem1  33751  cos9thpiminplylem2  33752  cos9thpiminplylem3  33753  cos9thpiminply  33757  qqhcn  33960  esumpr2  34036  esumpfinval  34044  esumpfinvalf  34045  carsggect  34288  oddpwdcv  34325  eulerpartlemgs2  34350  fibp1  34371  orvcelval  34439  ballotlemscr  34489  ballotlemfrci  34498  signsplypnf  34520  reprpmtf1o  34596  breprexplemc  34602  breprexp  34603  circlemeth  34610  lpadright  34654  revwlk  35100  subfacp1lem5  35159  cvmliftlem10  35269  circum  35649  faclimlem3  35720  fwddifnp1  36141  bj-bary1lem  37286  tan2h  37594  poimirlem3  37605  poimirlem13  37615  poimirlem14  37616  itgaddnclem1  37660  itgmulc2nclem2  37669  areacirclem1  37690  areacirclem4  37693  istotbnd3  37753  iscringd  37980  3atlem1  39465  pmod2iN  39831  polval2N  39888  lhple  40024  cdleme2  40210  cdleme35d  40434  cdleme42h  40464  cdlemeg46ngfr  40500  cdlemkid1  40904  lcfl7lem  41481  mapdpglem22  41675  mapdh6dN  41721  hdmap1l6d  41795  hdmapinvlem3  41902  lcmineqlem3  42007  nnadddir  42246  readvrec2  42337  readdsub  42360  sn-negex12  42393  zmulcomlem  42443  selvvvval  42561  evlselv  42563  evlsmhpvvval  42571  prjspeclsp  42588  prjspner1  42602  3cubeslem3r  42663  diophin  42748  irrapxlem2  42799  pellexlem6  42810  pell1234qrmulcl  42831  rmxyval  42891  rmxyneg  42896  rmxyadd  42897  jm2.24  42939  jm2.25  42975  limexissupab  43259  omabs2  43308  tfsconcatrev  43324  naddwordnexlem4  43377  snhesn  43762  scottrankd  44224  radcnvrat  44290  binomcxplemnotnn0  44332  sub2times  45258  mul13d  45265  fperiodmullem  45288  fperiodmul  45289  isumneg  45587  climneg  45595  itgsinexp  45940  stoweidlem13  45998  stoweidlem42  46027  wallispilem4  46053  wallispilem5  46054  wallispi2lem1  46056  stirlinglem1  46059  stirlinglem3  46061  stirlinglem4  46062  stirlinglem5  46063  stirlinglem7  46065  stirlinglem10  46068  dirkertrigeqlem3  46085  fourierdlem30  46122  fourierdlem32  46124  fourierdlem42  46134  fourierdlem48  46139  fourierdlem49  46140  fourierdlem83  46174  sqwvfoura  46213  sqwvfourb  46214  etransclem2  46221  etransclem46  46265  sharhght  46850  imasetpreimafvbijlemfv  47390  fmtnorec3  47536  quad1  47608  requad1  47610  ushggricedg  47915  lmodvsmdi  48367  dmatALTbas  48390  ldepsprlem  48461  itcovalt2lem2lem2  48663  ackval3  48672  1subrec1sub  48694  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  itsclc0xyqsolr  48758  swapfid  49268  sinhpcosh  49729