Theorem 3eqtr2d 2777

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  fmptapd  7126  negsub  11442  neg2sub  11454  divmuleq  11860  divneg2  11879  nnadddir  12233  discr  14202  bcpasc  14283  hashgval2  14340  hashf1lem2  14418  relexpaddnn  15013  crim  15077  remullem  15090  isum1p  15806  geo2sum  15838  fallfacfwd  16001  fsumkthpow  16021  bpoly3  16023  bpoly4  16024  efi4p  16104  sinhval  16121  addcos  16141  cos2tsin  16146  demoivreALT  16168  rpnnen2lem11  16191  omeo  16335  pwp1fsum  16360  sadaddlem  16435  bitsres  16442  smumullem  16461  sqgcd  16531  expgcd  16532  eulerthlem2  16752  vfermltlALT  16773  pockthlem  16876  4sqlem10  16918  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  fuccocl  17934  resssetc  18059  resscatc  18076  uncfcurf  18205  yonedalem3b  18245  prdspjmhm  18797  grpinvid2  18968  imasgrp2  19031  mulgaddcomlem  19073  mulgmodid  19089  lagsubg2  19169  cntzsgrpcl  19309  cntzsubm  19313  sylow3lem2  19603  efgredleme  19718  ablsubsub  19792  ablsubsub4  19793  odadd2  19824  gex2abl  19826  pgpfac1lem3a  20053  pwspjmhmmgpd  20307  rngcid  20612  ringcid  20641  abvneg  20803  lmodfopne  20895  lsppr  21088  rngqiprngfulem4  21312  gzrngunit  21413  frlmsubgval  21745  frlmgsum  21752  psrass1  21942  resspsradd  21953  resspsrvsca  21955  mplcoe5  22018  mplmon2mul  22047  evlslem2  22057  evlsvarsrng  22085  coe1tm  22238  ply1fermltlchr  22277  evls1varsrng  22305  mamuass  22367  mavmulass  22514  mulmarep1gsum2  22539  mdetuni0  22586  maducoeval2  22605  madulid  22610  mat2pmatmul  22696  decpmatmulsumfsupp  22738  pmatcollpwlem  22745  pm2mpmhmlem1  22783  cmpfi  23373  cnconn  23387  txrest  23596  utopsnneiplem  24212  blcvx  24763  tcphcphlem2  25203  cphipval2  25208  cphipval  25210  rrx0  25364  minveclem2  25393  pjthlem1  25404  uniioovol  25546  uniioombllem2  25550  itg1addlem4  25666  mbfi1fseqlem5  25686  itg2mulc  25714  itg2monolem1  25717  itgaddlem1  25790  itgmulc2lem2  25800  dvrec  25922  lhop2  25982  ftc1lem5  26007  deg1submon1p  26118  plypf1  26177  coefv0  26213  coemulhi  26219  coemulc  26220  dgreq0  26230  dvply1  26250  vieta1  26278  aareccl  26292  aaliou3lem8  26311  dvtaylp  26335  mtest  26369  sineq0  26488  efif1olem2  26507  efif1olem4  26509  tanarg  26583  logtayl2  26626  nnlogbexp  26745  isosctrlem2  26783  chordthmlem2  26797  chordthmlem4  26799  heron  26802  dcubic1lem  26807  dcubic1  26809  mcubic  26811  dquart  26817  quart1lem  26819  quart1  26820  efiasin  26852  asinsin  26856  atancj  26874  efiatan  26876  atanlogaddlem  26877  cosatan  26885  atantan  26887  atans2  26895  log2cnv  26908  log2tlbnd  26909  birthdaylem2  26916  cxplim  26935  lgamgulmlem2  26993  wilthlem1  27031  basellem3  27046  musum  27154  musumsum  27155  muinv  27156  pclogsum  27178  mersenne  27190  dchrabs  27223  dchrinv  27224  lgseisenlem1  27338  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  lgsquad2lem1  27347  2lgslem1  27357  2sqmod  27399  chebbnd1lem3  27434  chpchtlim  27442  rplogsumlem2  27448  dchrisumlem2  27453  dchrmusum2  27457  mulog2sumlem1  27497  mulog2sumlem3  27499  vmalogdivsum2  27501  selberg4lem1  27523  pntrlog2bndlem2  27541  pntrlog2bndlem4  27543  pntibndlem2  27554  pntlemr  27565  pntlemf  27568  pntlemo  27570  addsdilem4  28146  mulsunif2lem  28161  halfcut  28450  bdayfinbndlem1  28459  ragcom  28766  colperpexlem1  28798  lmiisolem  28864  hypcgrlem2  28868  trgcopyeulem  28873  brbtwn2  28974  colinearalglem1  28975  colinearalglem2  28976  axcontlem2  29034  axcontlem8  29040  numedglnl  29213  clwlkclwwlklem2a  30068  numclwlk1lem1  30439  numclwlk1lem2  30440  numclwwlk2  30451  grpoinvid2  30600  ablodivdiv4  30625  smcnlem  30768  ipidsq  30781  ipasslem2  30903  minvecolem2  30946  hv2times  31132  pjhthlem1  31462  pjds3i  31784  ho2times  31890  opsqrlem6  32216  pjclem4  32270  pj3si  32278  csmdsymi  32405  ofoprabco  32737  fcnvgreu  32745  quad3d  32822  nn0diffz0  32867  swrdrndisj  33017  trsp2cyc  33184  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2  33194  conjga  33231  elrgspnlem1  33303  rlocmulval  33330  imaslmod  33413  1arithufdlem3  33606  deg1prod  33643  r1padd1  33668  mplvrpmrhm  33691  esplyfvaln  33718  frlmdim  33755  rrxdim  33758  lbsdiflsp0  33770  fedgmullem1  33773  fedgmullem2  33774  extdg1id  33810  ccfldextdgrr  33816  fldextrspunlem1  33819  constrrtlc1  33876  constrrtcclem  33878  constrrtcc  33879  constrrecl  33913  constrresqrtcl  33921  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  cos9thpiminplylem3  33928  cos9thpiminply  33932  qqhcn  34135  esumpr2  34211  esumpfinval  34219  esumpfinvalf  34220  carsggect  34462  oddpwdcv  34499  eulerpartlemgs2  34524  fibp1  34545  orvcelval  34613  ballotlemscr  34663  ballotlemfrci  34672  signsplypnf  34694  reprpmtf1o  34770  breprexplemc  34776  breprexp  34777  circlemeth  34784  lpadright  34828  revwlk  35307  subfacp1lem5  35366  cvmliftlem10  35476  circum  35856  faclimlem3  35927  fwddifnp1  36347  bj-bary1lem  37624  qdiff  37641  tan2h  37933  poimirlem3  37944  poimirlem13  37954  poimirlem14  37955  itgaddnclem1  37999  itgmulc2nclem2  38008  areacirclem1  38029  areacirclem4  38032  istotbnd3  38092  iscringd  38319  3atlem1  39929  pmod2iN  40295  polval2N  40352  lhple  40488  cdleme2  40674  cdleme35d  40898  cdleme42h  40928  cdlemeg46ngfr  40964  cdlemkid1  41368  lcfl7lem  41945  mapdpglem22  42139  mapdh6dN  42185  hdmap1l6d  42259  hdmapinvlem3  42366  lcmineqlem3  42470  readvrec2  42793  readdsub  42816  sn-negex12  42849  zmulcomlem  42912  selvvvval  43018  evlselv  43020  evlsmhpvvval  43028  prjspeclsp  43045  prjspner1  43059  3cubeslem3r  43119  diophin  43204  irrapxlem2  43251  pellexlem6  43262  pell1234qrmulcl  43283  rmxyval  43343  rmxyneg  43348  rmxyadd  43349  jm2.24  43391  jm2.25  43427  limexissupab  43711  omabs2  43760  tfsconcatrev  43776  naddwordnexlem4  43829  snhesn  44213  scottrankd  44675  radcnvrat  44741  binomcxplemnotnn0  44783  sub2times  45706  mul13d  45713  fperiodmullem  45736  fperiodmul  45737  isumneg  46032  climneg  46040  itgsinexp  46383  stoweidlem13  46441  stoweidlem42  46470  wallispilem4  46496  wallispilem5  46497  wallispi2lem1  46499  stirlinglem1  46502  stirlinglem3  46504  stirlinglem4  46505  stirlinglem5  46506  stirlinglem7  46508  stirlinglem10  46511  dirkertrigeqlem3  46528  fourierdlem30  46565  fourierdlem32  46567  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem83  46617  sqwvfoura  46656  sqwvfourb  46657  etransclem2  46664  etransclem46  46708  sharhght  47293  sin3t  47319  sin5tlem1  47321  sin5tlem3  47323  cos5t  47327  imasetpreimafvbijlemfv  47862  fmtnorec3  48011  quad1  48096  requad1  48098  ushggricedg  48403  lmodvsmdi  48855  dmatALTbas  48877  ldepsprlem  48948  itcovalt2lem2lem2  49150  ackval3  49159  1subrec1sub  49181  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  itsclc0xyqsolr  49245  swapfid  49754  sinhpcosh  50215