Theorem 3eqtr2d 2802

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

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

This theorem is used by:  fmptapd  7174  scottrankd  9942  negsub  11599  neg2sub  11611  divmuleq  12015  divneg2  12034  nnadddir  12387  discr  14377  bcpasc  14458  hashgval2  14515  hashf1lem2  14594  relexpaddnn  15197  crim  15275  remullem  15288  isum1p  16003  geo2sum  16035  fallfacfwd  16195  fsumkthpow  16215  bpoly3  16217  bpoly4  16218  efi4p  16298  sinhval  16315  addcos  16335  cos2tsin  16340  demoivreALT  16362  rpnnen2lem11  16385  omeo  16529  pwp1fsum  16554  sadaddlem  16629  bitsres  16636  smumullem  16655  sqgcd  16729  expgcd  16730  eulerthlem2  16952  vfermltlALT  16973  pockthlem  17076  4sqlem10  17118  vdwlem2  17153  vdwlem6  17157  vdwlem8  17159  fuccocl  18135  resssetc  18260  resscatc  18277  uncfcurf  18406  yonedalem3b  18446  prdspjmhm  19018  grpinvid2  19196  imasgrp2  19258  mulgaddcomlem  19300  mulgmodid  19316  lagsubg2  19402  cntzsgrpcl  19541  cntzsubm  19545  sylow3lem2  19835  efgredleme  19950  ablsubsub  20024  ablsubsub4  20025  odadd2  20056  gex2abl  20058  pgpfac1lem3a  20285  pwspjmhmmgpd  20550  rngcid  20880  ringcid  20909  abvneg  21076  lmodfopne  21168  lsppr  21361  rngqiprngfulem4  21603  gzrngunit  21732  frlmsubgval  22064  frlmgsum  22071  psrass1  22264  resspsradd  22275  resspsrvsca  22277  mplcoe5  22342  mplmon2mul  22371  evlslem2  22381  evlsvarsrng  22409  selvvvval  22444  coe1tm  22585  ply1fermltlchr  22623  evls1varsrng  22651  mamuass  22710  mavmulass  22857  mulmarep1gsum2  22882  mdetuni0  22929  maducoeval2  22948  madulid  22953  mat2pmatmul  23042  decpmatmulsumfsupp  23084  pmatcollpwlem  23091  pm2mpmhmlem1  23129  cmpfi  23719  cnconn  23733  txrest  23943  utopsnneiplem  24559  blcvx  25110  tcphcphlem2  25550  cphipval2  25555  cphipval  25557  rrx0  25711  minveclem2  25740  pjthlem1  25751  uniioovol  25893  uniioombllem2  25897  itg1addlem4  26013  mbfi1fseqlem5  26033  itg2mulc  26061  itg2monolem1  26064  itgaddlem1  26136  itgmulc2lem2  26146  dvrec  26268  lhop2  26328  ftc1lem5  26353  deg1submon1p  26464  plypf1  26524  coefv0  26560  coemulhi  26566  coemulc  26567  dgreq0  26577  dvply1  26598  vieta1  26628  aareccl  26646  aaliou3lem8  26665  dvtaylp  26690  mtest  26724  sineq0  26845  efif1olem2  26864  efif1olem4  26866  tanarg  26940  logtayl2  26983  nnlogbexp  27102  isosctrlem2  27140  chordthmlem2  27154  chordthmlem4  27156  heron  27159  dcubic1lem  27164  dcubic1  27166  mcubic  27168  dquart  27174  quart1lem  27176  quart1  27177  efiasin  27209  asinsin  27213  atancj  27231  efiatan  27233  atanlogaddlem  27234  cosatan  27242  atantan  27244  atans2  27252  log2cnv  27265  log2tlbnd  27266  birthdaylem2  27273  cxplim  27292  lgamgulmlem2  27350  wilthlem1  27388  basellem3  27403  musum  27511  musumsum  27512  muinv  27513  pclogsum  27535  mersenne  27547  dchrabs  27580  dchrinv  27581  lgseisenlem1  27695  lgsquadlem1  27700  lgsquadlem2  27701  lgsquadlem3  27702  lgsquad2lem1  27704  2lgslem1  27714  2sqmod  27756  chebbnd1lem3  27791  chpchtlim  27799  rplogsumlem2  27805  dchrisumlem2  27810  dchrmusum2  27814  mulog2sumlem1  27854  mulog2sumlem3  27856  vmalogdivsum2  27858  selberg4lem1  27880  pntrlog2bndlem2  27898  pntrlog2bndlem4  27900  pntibndlem2  27911  pntlemr  27922  pntlemf  27925  pntlemo  27927  addsdilem4  28533  mulsunif2lem  28548  halfcut  28837  bdayfinbndlem1  28846  ragcom  29166  colperpexlem1  29199  plngrotlem2  29259  plng3p  29268  lmiisolem  29294  hypcgrlem2  29299  trgcopyeulem  29305  brbtwn2  29476  colinearalglem1  29477  colinearalglem2  29478  axcontlem2  29536  axcontlem8  29542  numedglnl  29715  revwlk  30260  clwlkclwwlklem2a  30582  numclwlk1lem1  30963  numclwlk1lem2  30964  numclwwlk2  30975  grpoinvid2  31124  ablodivdiv4  31149  smcnlem  31292  ipidsq  31305  ipasslem2  31427  minvecolem2  31470  hv2times  31656  pjhthlem1  31986  pjds3i  32308  ho2times  32414  opsqrlem6  32740  pjclem4  32794  pj3si  32802  csmdsymi  32929  ofoprabco  33251  fcnvgreu  33259  quad3d  33334  nn0diffz0  33379  swrdrndisj  33511  trsp2cyc  33677  cycpmco2lem3  33682  cycpmco2lem4  33683  cycpmco2lem5  33684  cycpmco2lem6  33685  cycpmco2  33687  conjga  33724  elrgspnlem1  33796  rlocmulval  33824  rlocinvunit  33829  rlocisunit  33830  imaslmod  33907  1arithufdlem3  34071  deg1prod  34108  r1padd1  34133  selvply1rhmlem2  34146  mplvrpmrhm  34172  esplyfvaln  34199  frlmdim  34236  rrxdim  34239  lbsdiflsp0  34251  fedgmullem1  34254  fedgmullem2  34255  extdg1id  34291  ccfldextdgrr  34297  fldextrspunlem1  34300  constrrtlc1  34357  constrrtcclem  34359  constrrtcc  34360  constrrecl  34394  constrresqrtcl  34402  cos9thpiminplylem1  34407  cos9thpiminplylem2  34408  cos9thpiminplylem3  34409  cos9thpiminply  34413  qqhcn  34616  esumpr2  34692  esumpfinval  34700  esumpfinvalf  34701  carsggect  34943  oddpwdcv  34980  eulerpartlemgs2  35005  fibp1  35026  orvcelval  35094  ballotlemscr  35144  ballotlemfrci  35153  signsplypnf  35172  reprpmtf1o  35248  breprexplemc  35254  breprexp  35255  circlemeth  35262  lpadright  35309  subfacp1lem5  35928  cvmliftlem10  36038  circum  36418  faclimlem3  36489  fwddifnp1  36910  bj-bary1lem  38211  qdiff  38228  tan2h  38515  poimirlem3  38521  poimirlem13  38531  poimirlem14  38532  itgaddnclem1  38576  itgmulc2nclem2  38585  areacirclem1  38606  areacirclem4  38609  istotbnd3  38685  iscringd  38912  3atlem1  40520  pmod2iN  40886  polval2N  40943  lhple  41079  cdleme2  41265  cdleme35d  41489  cdleme42h  41519  cdlemeg46ngfr  41555  cdlemkid1  41959  lcfl7lem  42536  mapdpglem22  42730  mapdh6dN  42776  hdmap1l6d  42850  hdmapinvlem3  42957  lcmineqlem3  43061  readvrec2  43392  readdsub  43415  sn-negex12  43448  zmulcomlem  43511  evlselv  43597  evlsmhpvvval  43603  prjspeclsp  43620  3cubeslem3r  43677  diophin  43762  irrapxlem2  43809  pellexlem6  43820  pell1234qrmulcl  43841  rmxyval  43901  rmxyneg  43906  rmxyadd  43907  jm2.24  43949  jm2.25  43985  limexissupab  44269  omabs2  44318  tfsconcatrev  44334  naddwordnexlem4  44387  snhesn  44771  radcnvrat  45283  binomcxplemnotnn0  45325  sub2times  46258  mul13d  46265  fperiodmullem  46288  fperiodmul  46289  isumneg  46583  climneg  46591  itgsinexp  46934  stoweidlem13  46992  stoweidlem42  47021  wallispilem4  47047  wallispilem5  47048  wallispi2lem1  47050  stirlinglem1  47053  stirlinglem3  47055  stirlinglem4  47056  stirlinglem5  47057  stirlinglem7  47059  stirlinglem10  47062  dirkertrigeqlem3  47079  fourierdlem30  47116  fourierdlem32  47118  fourierdlem42  47128  fourierdlem48  47133  fourierdlem49  47134  fourierdlem83  47168  sqwvfoura  47207  sqwvfourb  47208  etransclem2  47215  etransclem46  47259  sharhght  47844  sin3t  47886  sin5tlem1  47888  sin5tlem3  47890  cos5t  47894  imasetpreimafvbijlemfv  48453  fmtnorec3  48602  quad1  48687  requad1  48689  ushggricedg  48994  lmodvsmdi  49460  dmatALTbas  49482  ldepsprlem  49553  itcovalt2lem2lem2  49755  ackval3  49764  1subrec1sub  49786  eenglngeehlnmlem1  49818  eenglngeehlnmlem2  49819  itsclc0xyqsolr  49850  swapfid  50356  sinhpcosh  50802