Theorem 3eqtr2d 2801

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  fmptapd  7177  scottrankd  9953  negsub  11610  neg2sub  11622  divmuleq  12026  divneg2  12045  nnadddir  12398  discr  14388  bcpasc  14469  hashgval2  14526  hashf1lem2  14605  relexpaddnn  15210  crim  15288  remullem  15301  isum1p  16016  geo2sum  16048  fallfacfwd  16208  fsumkthpow  16228  bpoly3  16230  bpoly4  16231  efi4p  16311  sinhval  16328  addcos  16348  cos2tsin  16353  demoivreALT  16375  rpnnen2lem11  16398  omeo  16542  pwp1fsum  16567  sadaddlem  16642  bitsres  16649  smumullem  16668  sqgcd  16742  expgcd  16743  eulerthlem2  16965  vfermltlALT  16986  pockthlem  17089  4sqlem10  17131  vdwlem2  17166  vdwlem6  17170  vdwlem8  17172  fuccocl  18148  resssetc  18273  resscatc  18290  uncfcurf  18419  yonedalem3b  18459  prdspjmhm  19031  grpinvid2  19209  imasgrp2  19271  mulgaddcomlem  19313  mulgmodid  19329  lagsubg2  19415  cntzsgrpcl  19554  cntzsubm  19558  sylow3lem2  19848  efgredleme  19963  ablsubsub  20037  ablsubsub4  20038  odadd2  20069  gex2abl  20071  pgpfac1lem3a  20298  pwspjmhmmgpd  20563  rngcid  20893  ringcid  20922  abvneg  21089  lmodfopne  21181  lsppr  21374  rngqiprngfulem4  21616  gzrngunit  21745  frlmsubgval  22077  frlmgsum  22084  psrass1  22277  resspsradd  22288  resspsrvsca  22290  mplcoe5  22355  mplmon2mul  22384  evlslem2  22394  evlsvarsrng  22422  selvvvval  22457  coe1tm  22598  ply1fermltlchr  22636  evls1varsrng  22664  mamuass  22723  mavmulass  22870  mulmarep1gsum2  22895  mdetuni0  22942  maducoeval2  22961  madulid  22966  mat2pmatmul  23055  decpmatmulsumfsupp  23097  pmatcollpwlem  23104  pm2mpmhmlem1  23142  cmpfi  23732  cnconn  23746  txrest  23956  utopsnneiplem  24572  blcvx  25123  tcphcphlem2  25563  cphipval2  25568  cphipval  25570  rrx0  25724  minveclem2  25753  pjthlem1  25764  uniioovol  25906  uniioombllem2  25910  itg1addlem4  26026  mbfi1fseqlem5  26046  itg2mulc  26074  itg2monolem1  26077  itgaddlem1  26149  itgmulc2lem2  26159  dvrec  26281  lhop2  26341  ftc1lem5  26366  deg1submon1p  26477  plypf1  26537  coefv0  26573  coemulhi  26579  coemulc  26580  dgreq0  26590  dvply1  26611  vieta1  26641  aareccl  26659  aaliou3lem8  26678  dvtaylp  26703  mtest  26737  sineq0  26858  efif1olem2  26877  efif1olem4  26879  tanarg  26953  logtayl2  26996  nnlogbexp  27115  isosctrlem2  27153  chordthmlem2  27167  chordthmlem4  27169  heron  27172  dcubic1lem  27177  dcubic1  27179  mcubic  27181  dquart  27187  quart1lem  27189  quart1  27190  efiasin  27222  asinsin  27226  atancj  27244  efiatan  27246  atanlogaddlem  27247  cosatan  27255  atantan  27257  atans2  27265  log2cnv  27278  log2tlbnd  27279  birthdaylem2  27286  cxplim  27305  lgamgulmlem2  27363  wilthlem1  27401  basellem3  27416  musum  27524  musumsum  27525  muinv  27526  pclogsum  27548  mersenne  27560  dchrabs  27593  dchrinv  27594  lgseisenlem1  27708  lgsquadlem1  27713  lgsquadlem2  27714  lgsquadlem3  27715  lgsquad2lem1  27717  2lgslem1  27727  2sqmod  27769  chebbnd1lem3  27804  chpchtlim  27812  rplogsumlem2  27818  dchrisumlem2  27823  dchrmusum2  27827  mulog2sumlem1  27867  mulog2sumlem3  27869  vmalogdivsum2  27871  selberg4lem1  27893  pntrlog2bndlem2  27911  pntrlog2bndlem4  27913  pntibndlem2  27924  pntlemr  27935  pntlemf  27938  pntlemo  27940  addsdilem4  28546  mulsunif2lem  28561  halfcut  28850  bdayfinbndlem1  28859  ragcom  29179  colperpexlem1  29212  plngrotlem2  29272  plng3p  29281  lmiisolem  29307  hypcgrlem2  29312  trgcopyeulem  29318  brbtwn2  29489  colinearalglem1  29490  colinearalglem2  29491  axcontlem2  29549  axcontlem8  29555  numedglnl  29728  revwlk  30273  clwlkclwwlklem2a  30595  numclwlk1lem1  30976  numclwlk1lem2  30977  numclwwlk2  30988  grpoinvid2  31137  ablodivdiv4  31162  smcnlem  31305  ipidsq  31318  ipasslem2  31440  minvecolem2  31483  hv2times  31669  pjhthlem1  31999  pjds3i  32321  ho2times  32427  opsqrlem6  32753  pjclem4  32807  pj3si  32815  csmdsymi  32942  ofoprabco  33306  fcnvgreu  33314  quad3d  33388  nn0diffz0  33433  swrdrndisj  33565  trsp2cyc  33731  cycpmco2lem3  33736  cycpmco2lem4  33737  cycpmco2lem5  33738  cycpmco2lem6  33739  cycpmco2  33741  conjga  33778  elrgspnlem1  33850  rlocmulval  33878  rlocinvunit  33883  rlocisunit  33884  imaslmod  33961  1arithufdlem3  34125  deg1prod  34162  r1padd1  34187  selvply1rhmlem2  34200  mplvrpmrhm  34226  esplyfvaln  34253  frlmdim  34290  rrxdim  34293  lbsdiflsp0  34305  fedgmullem1  34308  fedgmullem2  34309  extdg1id  34345  ccfldextdgrr  34351  fldextrspunlem1  34354  constrrtlc1  34411  constrrtcclem  34413  constrrtcc  34414  constrrecl  34448  constrresqrtcl  34456  cos9thpiminplylem1  34461  cos9thpiminplylem2  34462  cos9thpiminplylem3  34463  cos9thpiminply  34467  qqhcn  34670  esumpr2  34746  esumpfinval  34754  esumpfinvalf  34755  carsggect  34997  oddpwdcv  35034  eulerpartlemgs2  35059  fibp1  35080  orvcelval  35148  ballotlemscr  35198  ballotlemfrci  35207  signsplypnf  35226  reprpmtf1o  35302  breprexplemc  35308  breprexp  35309  circlemeth  35316  lpadright  35363  subfacp1lem5  36036  cvmliftlem10  36146  circum  36526  faclimlem3  36603  fwddifnp1  37023  bj-bary1lem  38325  qdiff  38342  tan2h  38629  poimirlem3  38635  poimirlem13  38645  poimirlem14  38646  itgaddnclem1  38690  itgmulc2nclem2  38699  areacirclem1  38720  areacirclem4  38723  istotbnd3  38799  iscringd  39026  3atlem1  40634  pmod2iN  41000  polval2N  41057  lhple  41193  cdleme2  41379  cdleme35d  41603  cdleme42h  41633  cdlemeg46ngfr  41669  cdlemkid1  42073  lcfl7lem  42650  mapdpglem22  42844  mapdh6dN  42890  hdmap1l6d  42964  hdmapinvlem3  43071  lcmineqlem3  43175  readvrec2  43506  readdsub  43529  sn-negex12  43562  zmulcomlem  43625  evlselv  43711  evlsmhpvvval  43717  prjspeclsp  43734  3cubeslem3r  43791  diophin  43877  irrapxlem2  43924  pellexlem6  43935  pell1234qrmulcl  43956  rmxyval  44016  rmxyneg  44021  rmxyadd  44022  jm2.24  44064  jm2.25  44100  limexissupab  44379  omabs2  44428  tfsconcatrev  44444  naddwordnexlem4  44497  snhesn  44880  radcnvrat  45392  binomcxplemnotnn0  45434  sub2times  46383  mul13d  46390  fperiodmullem  46413  fperiodmul  46414  isumneg  46708  climneg  46716  itgsinexp  47059  stoweidlem13  47117  stoweidlem42  47146  wallispilem4  47172  wallispilem5  47173  wallispi2lem1  47175  stirlinglem1  47178  stirlinglem3  47180  stirlinglem4  47181  stirlinglem5  47182  stirlinglem7  47184  stirlinglem10  47187  dirkertrigeqlem3  47204  fourierdlem30  47241  fourierdlem32  47243  fourierdlem42  47253  fourierdlem48  47258  fourierdlem49  47259  fourierdlem83  47293  sqwvfoura  47332  sqwvfourb  47333  etransclem2  47340  etransclem46  47384  sharhght  47969  sin3t  48011  sin5tlem1  48013  sin5tlem3  48015  cos5t  48019  imasetpreimafvbijlemfv  48578  fmtnorec3  48727  quad1  48812  requad1  48814  ushggricedg  49119  lmodvsmdi  49585  dmatALTbas  49607  ldepsprlem  49678  itcovalt2lem2lem2  49880  ackval3  49889  1subrec1sub  49911  eenglngeehlnmlem1  49944  eenglngeehlnmlem2  49945  itsclc0xyqsolr  49975  swapfid  50495  sinhpcosh  51002