Theorem 3eqtr2d 2775

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

Syntax hints:   → wi 4   = wceq 1534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2721

This theorem is referenced by:  fmptapd  7187  negsub  11559  neg2sub  11571  divmuleq  11974  divneg2  11993  discr  14263  bcpasc  14344  hashgval2  14401  hashf1lem2  14479  relexpaddnn  15069  crim  15133  remullem  15146  isum1p  15858  geo2sum  15890  fallfacfwd  16051  fsumkthpow  16071  bpoly3  16073  bpoly4  16074  efi4p  16152  sinhval  16169  addcos  16189  cos2tsin  16194  demoivreALT  16216  rpnnen2lem11  16239  omeo  16381  pwp1fsum  16406  sadaddlem  16479  bitsres  16486  smumullem  16505  sqgcd  16576  expgcd  16577  eulerthlem2  16797  vfermltlALT  16817  pockthlem  16920  4sqlem10  16962  vdwlem2  16997  vdwlem6  17001  vdwlem8  17003  fuccocl  18002  resssetc  18127  resscatc  18144  uncfcurf  18277  yonedalem3b  18317  prdspjmhm  18832  grpinvid2  19000  imasgrp2  19063  mulgaddcomlem  19105  mulgmodid  19121  lagsubg2  19202  cntzsgrpcl  19342  cntzsubm  19346  sylow3lem2  19638  efgredleme  19753  ablsubsub  19827  ablsubsub4  19828  odadd2  19859  gex2abl  19861  pgpfac1lem3a  20088  pwspjmhmmgpd  20319  rngcid  20625  ringcid  20654  abvneg  20817  lmodfopne  20888  lsppr  21083  rngqiprngfulem4  21315  gzrngunit  21442  frlmsubgval  21776  frlmgsum  21783  psrass1  21974  resspsradd  21985  resspsrvsca  21987  mplcoe5  22048  mplmon2mul  22083  evlslem2  22093  evlsvarsrng  22113  coe1tm  22263  ply1scl1OLD  22284  ply1fermltlchr  22303  evls1varsrng  22331  mamuass  22393  mavmulass  22542  mulmarep1gsum2  22567  mdetuni0  22614  maducoeval2  22633  madulid  22638  mat2pmatmul  22724  decpmatmulsumfsupp  22766  pmatcollpwlem  22773  pm2mpmhmlem1  22811  cmpfi  23403  cnconn  23417  txrest  23626  utopsnneiplem  24243  blcvx  24805  tcphcphlem2  25255  cphipval2  25260  cphipval  25262  rrx0  25416  minveclem2  25445  pjthlem1  25456  uniioovol  25599  uniioombllem2  25603  itg1addlem4  25719  itg1addlem4OLD  25720  mbfi1fseqlem5  25740  itg2mulc  25768  itg2monolem1  25771  itgaddlem1  25843  itgmulc2lem2  25853  dvrec  25978  lhop2  26039  ftc1lem5  26066  deg1submon1p  26177  plypf1  26236  coefv0  26272  coemulhi  26278  coemulc  26279  dgreq0  26290  dvply1  26308  vieta1  26337  aareccl  26351  aaliou3lem8  26370  dvtaylp  26395  mtest  26430  sineq0  26548  efif1olem2  26567  efif1olem4  26569  tanarg  26643  logtayl2  26686  nnlogbexp  26806  isosctrlem2  26844  chordthmlem2  26858  chordthmlem4  26860  heron  26863  dcubic1lem  26868  dcubic1  26870  mcubic  26872  dquart  26878  quart1lem  26880  quart1  26881  efiasin  26913  asinsin  26917  atancj  26935  efiatan  26937  atanlogaddlem  26938  cosatan  26946  atantan  26948  atans2  26956  log2cnv  26969  log2tlbnd  26970  birthdaylem2  26977  cxplim  26997  lgamgulmlem2  27055  wilthlem1  27093  basellem3  27108  musum  27216  musumsum  27217  muinv  27218  pclogsum  27241  mersenne  27253  dchrabs  27286  dchrinv  27287  lgseisenlem1  27401  lgsquadlem1  27406  lgsquadlem2  27407  lgsquadlem3  27408  lgsquad2lem1  27410  2lgslem1  27420  2sqmod  27462  chebbnd1lem3  27497  chpchtlim  27505  rplogsumlem2  27511  dchrisumlem2  27516  dchrmusum2  27520  mulog2sumlem1  27560  mulog2sumlem3  27562  vmalogdivsum2  27564  selberg4lem1  27586  pntrlog2bndlem2  27604  pntrlog2bndlem4  27606  pntibndlem2  27617  pntlemr  27628  pntlemf  27631  pntlemo  27633  addsdilem4  28154  mulsunif2lem  28169  halfcut  28380  ragcom  28667  colperpexlem1  28699  lmiisolem  28765  hypcgrlem2  28769  trgcopyeulem  28774  brbtwn2  28881  colinearalglem1  28882  colinearalglem2  28883  axcontlem2  28941  axcontlem8  28947  numedglnl  29122  clwlkclwwlklem2a  29973  numclwlk1lem1  30344  numclwlk1lem2  30345  numclwwlk2  30356  grpoinvid2  30504  ablodivdiv4  30529  smcnlem  30672  ipidsq  30685  ipasslem2  30807  minvecolem2  30850  hv2times  31036  pjhthlem1  31366  pjds3i  31688  ho2times  31794  opsqrlem6  32120  pjclem4  32174  pj3si  32182  csmdsymi  32309  ofoprabco  32627  fcnvgreu  32636  quad3d  32702  swrdrndisj  32869  trsp2cyc  33061  cycpmco2lem3  33066  cycpmco2lem4  33067  cycpmco2lem5  33068  cycpmco2lem6  33069  cycpmco2  33071  rlocmulval  33186  imaslmod  33291  1arithufdlem3  33484  r1padd1  33538  frlmdim  33569  rrxdim  33572  lbsdiflsp0  33584  fedgmullem1  33587  fedgmullem2  33588  extdg1id  33621  ccfldextdgrr  33627  constrrtlc1  33668  constrrtcclem  33670  constrrtcc  33671  qqhcn  33882  esumpr2  33976  esumpfinval  33984  esumpfinvalf  33985  carsggect  34228  oddpwdcv  34265  eulerpartlemgs2  34290  fibp1  34311  orvcelval  34378  ballotlemscr  34428  ballotlemfrci  34437  signsplypnf  34472  reprpmtf1o  34548  breprexplemc  34554  breprexp  34555  circlemeth  34562  lpadright  34606  revwlk  35037  subfacp1lem5  35097  cvmliftlem10  35207  circum  35587  faclimlem3  35652  fwddifnp1  36074  bj-bary1lem  37102  tan2h  37398  poimirlem3  37409  poimirlem13  37419  poimirlem14  37420  itgaddnclem1  37464  itgmulc2nclem2  37473  areacirclem1  37494  areacirclem4  37497  istotbnd3  37557  iscringd  37784  3atlem1  39267  pmod2iN  39633  polval2N  39690  lhple  39826  cdleme2  40012  cdleme35d  40236  cdleme42h  40266  cdlemeg46ngfr  40302  cdlemkid1  40706  lcfl7lem  41283  mapdpglem22  41477  mapdh6dN  41523  hdmap1l6d  41597  hdmapinvlem3  41704  lcmineqlem3  41815  nnadddir  42084  readdsub  42170  sn-negex12  42202  zmulcomlem  42241  selvvvval  42350  evlselv  42352  evlsmhpvvval  42360  prjspeclsp  42377  prjspner1  42391  3cubeslem3r  42456  diophin  42541  irrapxlem2  42592  pellexlem6  42603  pell1234qrmulcl  42624  rmxyval  42685  rmxyneg  42690  rmxyadd  42691  jm2.24  42733  jm2.25  42769  limexissupab  43061  omabs2  43110  tfsconcatrev  43126  naddwordnexlem4  43180  snhesn  43565  scottrankd  44034  radcnvrat  44100  binomcxplemnotnn0  44142  sub2times  44998  mul13d  45005  fperiodmullem  45029  fperiodmul  45030  isumneg  45334  climneg  45342  itgsinexp  45687  stoweidlem13  45745  stoweidlem42  45774  wallispilem4  45800  wallispilem5  45801  wallispi2lem1  45803  stirlinglem1  45806  stirlinglem3  45808  stirlinglem4  45809  stirlinglem5  45810  stirlinglem7  45812  stirlinglem10  45815  dirkertrigeqlem3  45832  fourierdlem30  45869  fourierdlem32  45871  fourierdlem42  45881  fourierdlem48  45886  fourierdlem49  45887  fourierdlem83  45921  sqwvfoura  45960  sqwvfourb  45961  etransclem2  45968  etransclem46  46012  sharhght  46597  imasetpreimafvbijlemfv  47085  fmtnorec3  47231  quad1  47303  requad1  47305  ushggricedg  47586  lmodvsmdi  47883  dmatALTbas  47906  ldepsprlem  47977  itcovalt2lem2lem2  48184  ackval3  48193  1subrec1sub  48215  eenglngeehlnmlem1  48247  eenglngeehlnmlem2  48248  itsclc0xyqsolr  48279  sinhpcosh  48608