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 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  fmptapd  7169  scottrankd  9888  negsub  11530  neg2sub  11542  divmuleq  11944  divneg2  11963  nnadddir  12316  discr  14304  bcpasc  14385  hashgval2  14442  hashf1lem2  14521  relexpaddnn  15124  crim  15202  remullem  15215  isum1p  15930  geo2sum  15962  fallfacfwd  16122  fsumkthpow  16142  bpoly3  16144  bpoly4  16145  efi4p  16225  sinhval  16242  addcos  16262  cos2tsin  16267  demoivreALT  16289  rpnnen2lem11  16312  omeo  16456  pwp1fsum  16481  sadaddlem  16556  bitsres  16563  smumullem  16582  sqgcd  16652  expgcd  16653  eulerthlem2  16873  vfermltlALT  16894  pockthlem  16997  4sqlem10  17039  vdwlem2  17074  vdwlem6  17078  vdwlem8  17080  fuccocl  18056  resssetc  18181  resscatc  18198  uncfcurf  18327  yonedalem3b  18367  prdspjmhm  18938  grpinvid2  19116  imasgrp2  19178  mulgaddcomlem  19220  mulgmodid  19236  lagsubg2  19322  cntzsgrpcl  19461  cntzsubm  19465  sylow3lem2  19755  efgredleme  19870  ablsubsub  19944  ablsubsub4  19945  odadd2  19976  gex2abl  19978  pgpfac1lem3a  20205  pwspjmhmmgpd  20468  rngcid  20797  ringcid  20826  abvneg  20992  lmodfopne  21084  lsppr  21277  rngqiprngfulem4  21517  gzrngunit  21646  frlmsubgval  21978  frlmgsum  21985  psrass1  22178  resspsradd  22189  resspsrvsca  22191  mplcoe5  22256  mplmon2mul  22285  evlslem2  22295  evlsvarsrng  22323  selvvvval  22358  coe1tm  22499  ply1fermltlchr  22537  evls1varsrng  22565  mamuass  22624  mavmulass  22771  mulmarep1gsum2  22796  mdetuni0  22843  maducoeval2  22862  madulid  22867  mat2pmatmul  22956  decpmatmulsumfsupp  22998  pmatcollpwlem  23005  pm2mpmhmlem1  23043  cmpfi  23633  cnconn  23647  txrest  23857  utopsnneiplem  24473  blcvx  25024  tcphcphlem2  25464  cphipval2  25469  cphipval  25471  rrx0  25625  minveclem2  25654  pjthlem1  25665  uniioovol  25807  uniioombllem2  25811  itg1addlem4  25927  mbfi1fseqlem5  25947  itg2mulc  25975  itg2monolem1  25978  itgaddlem1  26050  itgmulc2lem2  26060  dvrec  26182  lhop2  26242  ftc1lem5  26267  deg1submon1p  26378  plypf1  26438  coefv0  26474  coemulhi  26480  coemulc  26481  dgreq0  26491  dvply1  26514  vieta1  26544  aareccl  26562  aaliou3lem8  26581  dvtaylp  26606  mtest  26640  sineq0  26761  efif1olem2  26780  efif1olem4  26782  tanarg  26856  logtayl2  26899  nnlogbexp  27018  isosctrlem2  27056  chordthmlem2  27070  chordthmlem4  27072  heron  27075  dcubic1lem  27080  dcubic1  27082  mcubic  27084  dquart  27090  quart1lem  27092  quart1  27093  efiasin  27125  asinsin  27129  atancj  27147  efiatan  27149  atanlogaddlem  27150  cosatan  27158  atantan  27160  atans2  27168  log2cnv  27181  log2tlbnd  27182  birthdaylem2  27189  cxplim  27208  lgamgulmlem2  27266  wilthlem1  27304  basellem3  27319  musum  27427  musumsum  27428  muinv  27429  pclogsum  27451  mersenne  27463  dchrabs  27496  dchrinv  27497  lgseisenlem1  27611  lgsquadlem1  27616  lgsquadlem2  27617  lgsquadlem3  27618  lgsquad2lem1  27620  2lgslem1  27630  2sqmod  27672  chebbnd1lem3  27707  chpchtlim  27715  rplogsumlem2  27721  dchrisumlem2  27726  dchrmusum2  27730  mulog2sumlem1  27770  mulog2sumlem3  27772  vmalogdivsum2  27774  selberg4lem1  27796  pntrlog2bndlem2  27814  pntrlog2bndlem4  27816  pntibndlem2  27827  pntlemr  27838  pntlemf  27841  pntlemo  27843  addsdilem4  28419  mulsunif2lem  28434  halfcut  28723  bdayfinbndlem1  28732  ragcom  29052  colperpexlem1  29085  plngrotlem2  29145  plng3p  29154  lmiisolem  29180  hypcgrlem2  29185  trgcopyeulem  29191  brbtwn2  29362  colinearalglem1  29363  colinearalglem2  29364  axcontlem2  29422  axcontlem8  29428  numedglnl  29601  revwlk  30146  clwlkclwwlklem2a  30468  numclwlk1lem1  30849  numclwlk1lem2  30850  numclwwlk2  30861  grpoinvid2  31010  ablodivdiv4  31035  smcnlem  31178  ipidsq  31191  ipasslem2  31313  minvecolem2  31356  hv2times  31542  pjhthlem1  31872  pjds3i  32194  ho2times  32300  opsqrlem6  32626  pjclem4  32680  pj3si  32688  csmdsymi  32815  ofoprabco  33137  fcnvgreu  33145  quad3d  33220  nn0diffz0  33265  swrdrndisj  33397  trsp2cyc  33563  cycpmco2lem3  33568  cycpmco2lem4  33569  cycpmco2lem5  33570  cycpmco2lem6  33571  cycpmco2  33573  conjga  33610  elrgspnlem1  33682  rlocmulval  33710  rlocinvunit  33715  rlocisunit  33716  imaslmod  33793  1arithufdlem3  33956  deg1prod  33993  r1padd1  34018  selvply1rhmlem2  34031  mplvrpmrhm  34057  esplyfvaln  34084  frlmdim  34121  rrxdim  34124  lbsdiflsp0  34136  fedgmullem1  34139  fedgmullem2  34140  extdg1id  34176  ccfldextdgrr  34182  fldextrspunlem1  34185  constrrtlc1  34242  constrrtcclem  34244  constrrtcc  34245  constrrecl  34279  constrresqrtcl  34287  cos9thpiminplylem1  34292  cos9thpiminplylem2  34293  cos9thpiminplylem3  34294  cos9thpiminply  34298  qqhcn  34501  esumpr2  34577  esumpfinval  34585  esumpfinvalf  34586  carsggect  34829  oddpwdcv  34866  eulerpartlemgs2  34891  fibp1  34912  orvcelval  34980  ballotlemscr  35030  ballotlemfrci  35039  signsplypnf  35058  reprpmtf1o  35134  breprexplemc  35140  breprexp  35141  circlemeth  35148  lpadright  35195  subfacp1lem5  35763  cvmliftlem10  35873  circum  36253  faclimlem3  36324  fwddifnp1  36745  bj-bary1lem  38062  qdiff  38079  tan2h  38366  poimirlem3  38372  poimirlem13  38382  poimirlem14  38383  itgaddnclem1  38427  itgmulc2nclem2  38436  areacirclem1  38457  areacirclem4  38460  istotbnd3  38521  iscringd  38748  3atlem1  40356  pmod2iN  40722  polval2N  40779  lhple  40915  cdleme2  41101  cdleme35d  41325  cdleme42h  41355  cdlemeg46ngfr  41391  cdlemkid1  41795  lcfl7lem  42372  mapdpglem22  42566  mapdh6dN  42612  hdmap1l6d  42686  hdmapinvlem3  42793  lcmineqlem3  42897  readvrec2  43236  readdsub  43259  sn-negex12  43292  zmulcomlem  43355  evlselv  43435  evlsmhpvvval  43441  prjspeclsp  43458  prjspner1  43472  3cubeslem3r  43532  diophin  43617  irrapxlem2  43664  pellexlem6  43675  pell1234qrmulcl  43696  rmxyval  43756  rmxyneg  43761  rmxyadd  43762  jm2.24  43804  jm2.25  43840  limexissupab  44124  omabs2  44173  tfsconcatrev  44189  naddwordnexlem4  44242  snhesn  44626  radcnvrat  45138  binomcxplemnotnn0  45180  sub2times  46106  mul13d  46113  fperiodmullem  46136  fperiodmul  46137  isumneg  46432  climneg  46440  itgsinexp  46783  stoweidlem13  46841  stoweidlem42  46870  wallispilem4  46896  wallispilem5  46897  wallispi2lem1  46899  stirlinglem1  46902  stirlinglem3  46904  stirlinglem4  46905  stirlinglem5  46906  stirlinglem7  46908  stirlinglem10  46911  dirkertrigeqlem3  46928  fourierdlem30  46965  fourierdlem32  46967  fourierdlem42  46977  fourierdlem48  46982  fourierdlem49  46983  fourierdlem83  47017  sqwvfoura  47056  sqwvfourb  47057  etransclem2  47064  etransclem46  47108  sharhght  47693  sin3t  47735  sin5tlem1  47737  sin5tlem3  47739  cos5t  47743  imasetpreimafvbijlemfv  48302  fmtnorec3  48451  quad1  48536  requad1  48538  ushggricedg  48843  lmodvsmdi  49309  dmatALTbas  49331  ldepsprlem  49402  itcovalt2lem2lem2  49604  ackval3  49613  1subrec1sub  49635  eenglngeehlnmlem1  49667  eenglngeehlnmlem2  49668  itsclc0xyqsolr  49699  swapfid  50205  sinhpcosh  50666