Theorem 3eqtr2d 2778

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

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

This theorem is referenced by:  fmptapd  7119  negsub  11433  neg2sub  11445  divmuleq  11851  divneg2  11870  nnadddir  12224  discr  14193  bcpasc  14274  hashgval2  14331  hashf1lem2  14409  relexpaddnn  15004  crim  15068  remullem  15081  isum1p  15797  geo2sum  15829  fallfacfwd  15992  fsumkthpow  16012  bpoly3  16014  bpoly4  16015  efi4p  16095  sinhval  16112  addcos  16132  cos2tsin  16137  demoivreALT  16159  rpnnen2lem11  16182  omeo  16326  pwp1fsum  16351  sadaddlem  16426  bitsres  16433  smumullem  16452  sqgcd  16522  expgcd  16523  eulerthlem2  16743  vfermltlALT  16764  pockthlem  16867  4sqlem10  16909  vdwlem2  16944  vdwlem6  16948  vdwlem8  16950  fuccocl  17925  resssetc  18050  resscatc  18067  uncfcurf  18196  yonedalem3b  18236  prdspjmhm  18788  grpinvid2  18959  imasgrp2  19022  mulgaddcomlem  19064  mulgmodid  19080  lagsubg2  19160  cntzsgrpcl  19300  cntzsubm  19304  sylow3lem2  19594  efgredleme  19709  ablsubsub  19783  ablsubsub4  19784  odadd2  19815  gex2abl  19817  pgpfac1lem3a  20044  pwspjmhmmgpd  20298  rngcid  20603  ringcid  20632  abvneg  20794  lmodfopne  20886  lsppr  21080  rngqiprngfulem4  21304  gzrngunit  21423  frlmsubgval  21755  frlmgsum  21762  psrass1  21952  resspsradd  21963  resspsrvsca  21965  mplcoe5  22028  mplmon2mul  22057  evlslem2  22067  evlsvarsrng  22095  coe1tm  22248  ply1fermltlchr  22287  evls1varsrng  22315  mamuass  22377  mavmulass  22524  mulmarep1gsum2  22549  mdetuni0  22596  maducoeval2  22615  madulid  22620  mat2pmatmul  22706  decpmatmulsumfsupp  22748  pmatcollpwlem  22755  pm2mpmhmlem1  22793  cmpfi  23383  cnconn  23397  txrest  23606  utopsnneiplem  24222  blcvx  24773  tcphcphlem2  25213  cphipval2  25218  cphipval  25220  rrx0  25374  minveclem2  25403  pjthlem1  25414  uniioovol  25556  uniioombllem2  25560  itg1addlem4  25676  mbfi1fseqlem5  25696  itg2mulc  25724  itg2monolem1  25727  itgaddlem1  25800  itgmulc2lem2  25810  dvrec  25932  lhop2  25992  ftc1lem5  26017  deg1submon1p  26128  plypf1  26187  coefv0  26223  coemulhi  26229  coemulc  26230  dgreq0  26240  dvply1  26260  vieta1  26289  aareccl  26303  aaliou3lem8  26322  dvtaylp  26347  mtest  26382  sineq0  26501  efif1olem2  26520  efif1olem4  26522  tanarg  26596  logtayl2  26639  nnlogbexp  26758  isosctrlem2  26796  chordthmlem2  26810  chordthmlem4  26812  heron  26815  dcubic1lem  26820  dcubic1  26822  mcubic  26824  dquart  26830  quart1lem  26832  quart1  26833  efiasin  26865  asinsin  26869  atancj  26887  efiatan  26889  atanlogaddlem  26890  cosatan  26898  atantan  26900  atans2  26908  log2cnv  26921  log2tlbnd  26922  birthdaylem2  26929  cxplim  26949  lgamgulmlem2  27007  wilthlem1  27045  basellem3  27060  musum  27168  musumsum  27169  muinv  27170  pclogsum  27192  mersenne  27204  dchrabs  27237  dchrinv  27238  lgseisenlem1  27352  lgsquadlem1  27357  lgsquadlem2  27358  lgsquadlem3  27359  lgsquad2lem1  27361  2lgslem1  27371  2sqmod  27413  chebbnd1lem3  27448  chpchtlim  27456  rplogsumlem2  27462  dchrisumlem2  27467  dchrmusum2  27471  mulog2sumlem1  27511  mulog2sumlem3  27513  vmalogdivsum2  27515  selberg4lem1  27537  pntrlog2bndlem2  27555  pntrlog2bndlem4  27557  pntibndlem2  27568  pntlemr  27579  pntlemf  27582  pntlemo  27584  addsdilem4  28160  mulsunif2lem  28175  halfcut  28464  bdayfinbndlem1  28473  ragcom  28780  colperpexlem1  28812  lmiisolem  28878  hypcgrlem2  28882  trgcopyeulem  28887  brbtwn2  28988  colinearalglem1  28989  colinearalglem2  28990  axcontlem2  29048  axcontlem8  29054  numedglnl  29227  clwlkclwwlklem2a  30083  numclwlk1lem1  30454  numclwlk1lem2  30455  numclwwlk2  30466  grpoinvid2  30615  ablodivdiv4  30640  smcnlem  30783  ipidsq  30796  ipasslem2  30918  minvecolem2  30961  hv2times  31147  pjhthlem1  31477  pjds3i  31799  ho2times  31905  opsqrlem6  32231  pjclem4  32285  pj3si  32293  csmdsymi  32420  ofoprabco  32752  fcnvgreu  32760  quad3d  32837  nn0diffz0  32882  swrdrndisj  33032  trsp2cyc  33199  cycpmco2lem3  33204  cycpmco2lem4  33205  cycpmco2lem5  33206  cycpmco2lem6  33207  cycpmco2  33209  conjga  33246  elrgspnlem1  33318  rlocmulval  33345  imaslmod  33428  1arithufdlem3  33621  deg1prod  33658  r1padd1  33683  mplvrpmrhm  33706  esplyfvaln  33733  frlmdim  33771  rrxdim  33774  lbsdiflsp0  33786  fedgmullem1  33789  fedgmullem2  33790  extdg1id  33826  ccfldextdgrr  33832  fldextrspunlem1  33835  constrrtlc1  33892  constrrtcclem  33894  constrrtcc  33895  constrrecl  33929  constrresqrtcl  33937  cos9thpiminplylem1  33942  cos9thpiminplylem2  33943  cos9thpiminplylem3  33944  cos9thpiminply  33948  qqhcn  34151  esumpr2  34227  esumpfinval  34235  esumpfinvalf  34236  carsggect  34478  oddpwdcv  34515  eulerpartlemgs2  34540  fibp1  34561  orvcelval  34629  ballotlemscr  34679  ballotlemfrci  34688  signsplypnf  34710  reprpmtf1o  34786  breprexplemc  34792  breprexp  34793  circlemeth  34800  lpadright  34844  revwlk  35323  subfacp1lem5  35382  cvmliftlem10  35492  circum  35872  faclimlem3  35943  fwddifnp1  36363  bj-bary1lem  37640  tan2h  37947  poimirlem3  37958  poimirlem13  37968  poimirlem14  37969  itgaddnclem1  38013  itgmulc2nclem2  38022  areacirclem1  38043  areacirclem4  38046  istotbnd3  38106  iscringd  38333  3atlem1  39943  pmod2iN  40309  polval2N  40366  lhple  40502  cdleme2  40688  cdleme35d  40912  cdleme42h  40942  cdlemeg46ngfr  40978  cdlemkid1  41382  lcfl7lem  41959  mapdpglem22  42153  mapdh6dN  42199  hdmap1l6d  42273  hdmapinvlem3  42380  lcmineqlem3  42484  readvrec2  42807  readdsub  42830  sn-negex12  42863  zmulcomlem  42926  selvvvval  43032  evlselv  43034  evlsmhpvvval  43042  prjspeclsp  43059  prjspner1  43073  3cubeslem3r  43133  diophin  43218  irrapxlem2  43269  pellexlem6  43280  pell1234qrmulcl  43301  rmxyval  43361  rmxyneg  43366  rmxyadd  43367  jm2.24  43409  jm2.25  43445  limexissupab  43729  omabs2  43778  tfsconcatrev  43794  naddwordnexlem4  43847  snhesn  44231  scottrankd  44693  radcnvrat  44759  binomcxplemnotnn0  44801  sub2times  45724  mul13d  45731  fperiodmullem  45754  fperiodmul  45755  isumneg  46050  climneg  46058  itgsinexp  46401  stoweidlem13  46459  stoweidlem42  46488  wallispilem4  46514  wallispilem5  46515  wallispi2lem1  46517  stirlinglem1  46520  stirlinglem3  46522  stirlinglem4  46523  stirlinglem5  46524  stirlinglem7  46526  stirlinglem10  46529  dirkertrigeqlem3  46546  fourierdlem30  46583  fourierdlem32  46585  fourierdlem42  46595  fourierdlem48  46600  fourierdlem49  46601  fourierdlem83  46635  sqwvfoura  46674  sqwvfourb  46675  etransclem2  46682  etransclem46  46726  sharhght  47311  sin3t  47335  sin5tlem1  47337  sin5tlem3  47339  imasetpreimafvbijlemfv  47874  fmtnorec3  48023  quad1  48108  requad1  48110  ushggricedg  48415  lmodvsmdi  48867  dmatALTbas  48889  ldepsprlem  48960  itcovalt2lem2lem2  49162  ackval3  49171  1subrec1sub  49193  eenglngeehlnmlem1  49225  eenglngeehlnmlem2  49226  itsclc0xyqsolr  49257  swapfid  49766  sinhpcosh  50227