Theorem 3eqtr2d 2776

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  fmptapd  7162  negsub  11529  neg2sub  11541  divmuleq  11944  divneg2  11963  discr  14256  bcpasc  14337  hashgval2  14394  hashf1lem2  14472  relexpaddnn  15068  crim  15132  remullem  15145  isum1p  15855  geo2sum  15887  fallfacfwd  16050  fsumkthpow  16070  bpoly3  16072  bpoly4  16073  efi4p  16153  sinhval  16170  addcos  16190  cos2tsin  16195  demoivreALT  16217  rpnnen2lem11  16240  omeo  16383  pwp1fsum  16408  sadaddlem  16483  bitsres  16490  smumullem  16509  sqgcd  16579  expgcd  16580  eulerthlem2  16799  vfermltlALT  16820  pockthlem  16923  4sqlem10  16965  vdwlem2  17000  vdwlem6  17004  vdwlem8  17006  fuccocl  17978  resssetc  18103  resscatc  18120  uncfcurf  18249  yonedalem3b  18289  prdspjmhm  18805  grpinvid2  18973  imasgrp2  19036  mulgaddcomlem  19078  mulgmodid  19094  lagsubg2  19175  cntzsgrpcl  19315  cntzsubm  19319  sylow3lem2  19607  efgredleme  19722  ablsubsub  19796  ablsubsub4  19797  odadd2  19828  gex2abl  19830  pgpfac1lem3a  20057  pwspjmhmmgpd  20286  rngcid  20593  ringcid  20622  abvneg  20784  lmodfopne  20855  lsppr  21049  rngqiprngfulem4  21273  gzrngunit  21399  frlmsubgval  21723  frlmgsum  21730  psrass1  21922  resspsradd  21933  resspsrvsca  21935  mplcoe5  21996  mplmon2mul  22025  evlslem2  22035  evlsvarsrng  22055  coe1tm  22208  ply1scl1OLD  22229  ply1fermltlchr  22248  evls1varsrng  22276  mamuass  22338  mavmulass  22485  mulmarep1gsum2  22510  mdetuni0  22557  maducoeval2  22576  madulid  22581  mat2pmatmul  22667  decpmatmulsumfsupp  22709  pmatcollpwlem  22716  pm2mpmhmlem1  22754  cmpfi  23344  cnconn  23358  txrest  23567  utopsnneiplem  24184  blcvx  24735  tcphcphlem2  25186  cphipval2  25191  cphipval  25193  rrx0  25347  minveclem2  25376  pjthlem1  25387  uniioovol  25530  uniioombllem2  25534  itg1addlem4  25650  mbfi1fseqlem5  25670  itg2mulc  25698  itg2monolem1  25701  itgaddlem1  25774  itgmulc2lem2  25784  dvrec  25909  lhop2  25970  ftc1lem5  25997  deg1submon1p  26108  plypf1  26167  coefv0  26203  coemulhi  26209  coemulc  26210  dgreq0  26221  dvply1  26241  vieta1  26270  aareccl  26284  aaliou3lem8  26303  dvtaylp  26328  mtest  26363  sineq0  26483  efif1olem2  26502  efif1olem4  26504  tanarg  26578  logtayl2  26621  nnlogbexp  26741  isosctrlem2  26779  chordthmlem2  26793  chordthmlem4  26795  heron  26798  dcubic1lem  26803  dcubic1  26805  mcubic  26807  dquart  26813  quart1lem  26815  quart1  26816  efiasin  26848  asinsin  26852  atancj  26870  efiatan  26872  atanlogaddlem  26873  cosatan  26881  atantan  26883  atans2  26891  log2cnv  26904  log2tlbnd  26905  birthdaylem2  26912  cxplim  26932  lgamgulmlem2  26990  wilthlem1  27028  basellem3  27043  musum  27151  musumsum  27152  muinv  27153  pclogsum  27176  mersenne  27188  dchrabs  27221  dchrinv  27222  lgseisenlem1  27336  lgsquadlem1  27341  lgsquadlem2  27342  lgsquadlem3  27343  lgsquad2lem1  27345  2lgslem1  27355  2sqmod  27397  chebbnd1lem3  27432  chpchtlim  27440  rplogsumlem2  27446  dchrisumlem2  27451  dchrmusum2  27455  mulog2sumlem1  27495  mulog2sumlem3  27497  vmalogdivsum2  27499  selberg4lem1  27521  pntrlog2bndlem2  27539  pntrlog2bndlem4  27541  pntibndlem2  27552  pntlemr  27563  pntlemf  27566  pntlemo  27568  addsdilem4  28097  mulsunif2lem  28112  halfcut  28333  zs12bday  28341  ragcom  28623  colperpexlem1  28655  lmiisolem  28721  hypcgrlem2  28725  trgcopyeulem  28730  brbtwn2  28830  colinearalglem1  28831  colinearalglem2  28832  axcontlem2  28890  axcontlem8  28896  numedglnl  29069  clwlkclwwlklem2a  29925  numclwlk1lem1  30296  numclwlk1lem2  30297  numclwwlk2  30308  grpoinvid2  30456  ablodivdiv4  30481  smcnlem  30624  ipidsq  30637  ipasslem2  30759  minvecolem2  30802  hv2times  30988  pjhthlem1  31318  pjds3i  31640  ho2times  31746  opsqrlem6  32072  pjclem4  32126  pj3si  32134  csmdsymi  32261  ofoprabco  32588  fcnvgreu  32597  quad3d  32673  swrdrndisj  32879  trsp2cyc  33080  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2  33090  elrgspnlem1  33183  rlocmulval  33210  imaslmod  33314  1arithufdlem3  33507  r1padd1  33563  frlmdim  33597  rrxdim  33600  lbsdiflsp0  33612  fedgmullem1  33615  fedgmullem2  33616  extdg1id  33653  ccfldextdgrr  33659  fldextrspunlem1  33662  constrrtlc1  33712  constrrtcclem  33714  constrrtcc  33715  constrrecl  33749  constrresqrtcl  33757  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  cos9thpiminplylem3  33764  cos9thpiminply  33768  qqhcn  33968  esumpr2  34044  esumpfinval  34052  esumpfinvalf  34053  carsggect  34296  oddpwdcv  34333  eulerpartlemgs2  34358  fibp1  34379  orvcelval  34447  ballotlemscr  34497  ballotlemfrci  34506  signsplypnf  34528  reprpmtf1o  34604  breprexplemc  34610  breprexp  34611  circlemeth  34618  lpadright  34662  revwlk  35093  subfacp1lem5  35152  cvmliftlem10  35262  circum  35642  faclimlem3  35708  fwddifnp1  36129  bj-bary1lem  37274  tan2h  37582  poimirlem3  37593  poimirlem13  37603  poimirlem14  37604  itgaddnclem1  37648  itgmulc2nclem2  37657  areacirclem1  37678  areacirclem4  37681  istotbnd3  37741  iscringd  37968  3atlem1  39448  pmod2iN  39814  polval2N  39871  lhple  40007  cdleme2  40193  cdleme35d  40417  cdleme42h  40447  cdlemeg46ngfr  40483  cdlemkid1  40887  lcfl7lem  41464  mapdpglem22  41658  mapdh6dN  41704  hdmap1l6d  41778  hdmapinvlem3  41885  lcmineqlem3  41990  nnadddir  42267  readvrec2  42351  readdsub  42374  sn-negex12  42406  zmulcomlem  42445  selvvvval  42555  evlselv  42557  evlsmhpvvval  42565  prjspeclsp  42582  prjspner1  42596  3cubeslem3r  42657  diophin  42742  irrapxlem2  42793  pellexlem6  42804  pell1234qrmulcl  42825  rmxyval  42886  rmxyneg  42891  rmxyadd  42892  jm2.24  42934  jm2.25  42970  limexissupab  43254  omabs2  43303  tfsconcatrev  43319  naddwordnexlem4  43372  snhesn  43757  scottrankd  44220  radcnvrat  44286  binomcxplemnotnn0  44328  sub2times  45249  mul13d  45256  fperiodmullem  45280  fperiodmul  45281  isumneg  45579  climneg  45587  itgsinexp  45932  stoweidlem13  45990  stoweidlem42  46019  wallispilem4  46045  wallispilem5  46046  wallispi2lem1  46048  stirlinglem1  46051  stirlinglem3  46053  stirlinglem4  46054  stirlinglem5  46055  stirlinglem7  46057  stirlinglem10  46060  dirkertrigeqlem3  46077  fourierdlem30  46114  fourierdlem32  46116  fourierdlem42  46126  fourierdlem48  46131  fourierdlem49  46132  fourierdlem83  46166  sqwvfoura  46205  sqwvfourb  46206  etransclem2  46213  etransclem46  46257  sharhght  46842  imasetpreimafvbijlemfv  47364  fmtnorec3  47510  quad1  47582  requad1  47584  ushggricedg  47888  lmodvsmdi  48302  dmatALTbas  48325  ldepsprlem  48396  itcovalt2lem2lem2  48602  ackval3  48611  1subrec1sub  48633  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  itsclc0xyqsolr  48697  swapfid  49144  sinhpcosh  49552