Theorem 3eqtr2d 2862

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  fmptapd  6933  negsub  10934  neg2sub  10946  divmuleq  11345  divneg2  11364  discr  13602  bcpasc  13682  hashgval2  13740  hashf1lem2  13815  relexpaddnn  14410  crim  14474  remullem  14487  isum1p  15196  geo2sum  15229  fallfacfwd  15390  fsumkthpow  15410  bpoly3  15412  bpoly4  15413  efi4p  15490  sinhval  15507  addcos  15527  cos2tsin  15532  demoivreALT  15554  rpnnen2lem11  15577  omeo  15715  pwp1fsum  15742  sadaddlem  15815  bitsres  15822  smumullem  15841  sqgcd  15909  eulerthlem2  16119  vfermltlALT  16139  pockthlem  16241  4sqlem10  16283  vdwlem2  16318  vdwlem6  16322  vdwlem8  16324  fuccocl  17234  resssetc  17352  resscatc  17365  uncfcurf  17489  yonedalem3b  17529  prdspjmhm  17993  grpinvid2  18155  imasgrp2  18214  mulgaddcomlem  18250  mulgmodid  18266  lagsubg2  18341  cntzsubm  18466  sylow3lem2  18753  efgredleme  18869  ablsubsub  18938  ablsubsub4  18939  odadd2  18969  gex2abl  18971  pgpfac1lem3a  19198  abvneg  19605  lmodfopne  19672  lsppr  19865  psrass1  20185  resspsradd  20196  resspsrvsca  20198  mplcoe5  20249  mplmon2mul  20281  evlslem2  20292  evlsvarsrng  20312  coe1tm  20441  ply1scl1  20460  evls1varsrng  20503  gzrngunit  20611  frlmsubgval  20909  frlmgsum  20916  mamuass  21011  mavmulass  21158  mulmarep1gsum2  21183  mdetuni0  21230  maducoeval2  21249  madulid  21254  mat2pmatmul  21339  decpmatmulsumfsupp  21381  pmatcollpwlem  21388  pm2mpmhmlem1  21426  cmpfi  22016  cnconn  22030  txrest  22239  utopsnneiplem  22856  blcvx  23406  tcphcphlem2  23839  cphipval2  23844  cphipval  23846  rrx0  24000  minveclem2  24029  pjthlem1  24040  uniioovol  24180  uniioombllem2  24184  itg1addlem4  24300  mbfi1fseqlem5  24320  itg2mulc  24348  itg2monolem1  24351  itgaddlem1  24423  itgmulc2lem2  24433  dvrec  24552  lhop2  24612  ftc1lem5  24637  deg1submon1p  24746  plypf1  24802  coefv0  24838  coemulhi  24844  coemulc  24845  dgreq0  24855  dvply1  24873  vieta1  24901  aareccl  24915  aaliou3lem8  24934  dvtaylp  24958  mtest  24992  sineq0  25109  efif1olem2  25127  efif1olem4  25129  tanarg  25202  logtayl2  25245  nnlogbexp  25359  isosctrlem2  25397  chordthmlem2  25411  chordthmlem4  25413  heron  25416  dcubic1lem  25421  dcubic1  25423  mcubic  25425  dquart  25431  quart1lem  25433  quart1  25434  efiasin  25466  asinsin  25470  atancj  25488  efiatan  25490  atanlogaddlem  25491  cosatan  25499  atantan  25501  atans2  25509  log2cnv  25522  log2tlbnd  25523  birthdaylem2  25530  cxplim  25549  lgamgulmlem2  25607  wilthlem1  25645  basellem3  25660  musum  25768  musumsum  25769  muinv  25770  pclogsum  25791  mersenne  25803  dchrabs  25836  dchrinv  25837  lgseisenlem1  25951  lgsquadlem1  25956  lgsquadlem2  25957  lgsquadlem3  25958  lgsquad2lem1  25960  2lgslem1  25970  2sqmod  26012  chebbnd1lem3  26047  chpchtlim  26055  rplogsumlem2  26061  dchrisumlem2  26066  dchrmusum2  26070  mulog2sumlem1  26110  mulog2sumlem3  26112  vmalogdivsum2  26114  selberg4lem1  26136  pntrlog2bndlem2  26154  pntrlog2bndlem4  26156  pntibndlem2  26167  pntlemr  26178  pntlemf  26181  pntlemo  26183  ragcom  26484  colperpexlem1  26516  lmiisolem  26582  hypcgrlem2  26586  trgcopyeulem  26591  brbtwn2  26691  colinearalglem1  26692  colinearalglem2  26693  axcontlem2  26751  axcontlem8  26757  numedglnl  26929  clwlkclwwlklem2a  27776  numclwlk1lem1  28148  numclwlk1lem2  28149  numclwwlk2  28160  grpoinvid2  28306  ablodivdiv4  28331  smcnlem  28474  ipidsq  28487  ipasslem2  28609  minvecolem2  28652  hv2times  28838  pjhthlem1  29168  pjds3i  29490  ho2times  29596  opsqrlem6  29922  pjclem4  29976  pj3si  29984  csmdsymi  30111  ofoprabco  30409  fcnvgreu  30418  swrdrndisj  30631  trsp2cyc  30765  cycpmco2lem3  30770  cycpmco2lem4  30771  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2  30775  imaslmod  30922  frlmdim  31009  rrxdim  31012  lbsdiflsp0  31022  fedgmullem1  31025  fedgmullem2  31026  extdg1id  31053  ccfldextdgrr  31057  qqhcn  31232  esumpr2  31326  esumpfinval  31334  esumpfinvalf  31335  carsggect  31576  oddpwdcv  31613  eulerpartlemgs2  31638  fibp1  31659  orvcelval  31726  ballotlemscr  31776  ballotlemfrci  31785  signsplypnf  31820  reprpmtf1o  31897  breprexplemc  31903  breprexp  31904  circlemeth  31911  lpadright  31955  revwlk  32371  subfacp1lem5  32431  cvmliftlem10  32541  circum  32917  faclimlem3  32977  fwddifnp1  33626  bj-bary1lem  34594  tan2h  34899  poimirlem3  34910  poimirlem13  34920  poimirlem14  34921  itgaddnclem1  34965  itgmulc2nclem2  34974  areacirclem1  34997  areacirclem4  35000  istotbnd3  35064  iscringd  35291  3atlem1  36634  pmod2iN  37000  polval2N  37057  lhple  37193  cdleme2  37379  cdleme35d  37603  cdleme42h  37633  cdlemeg46ngfr  37669  cdlemkid1  38073  lcfl7lem  38650  mapdpglem22  38844  mapdh6dN  38890  hdmap1l6d  38964  hdmapinvlem3  39071  nnadddir  39212  expgcd  39232  readdsub  39263  prjspeclsp  39311  3cubeslem3r  39333  diophin  39418  irrapxlem2  39469  pellexlem6  39480  pell1234qrmulcl  39501  rmxyval  39561  rmxyneg  39566  rmxyadd  39567  jm2.24  39609  jm2.25  39645  snhesn  40181  scottrankd  40633  radcnvrat  40695  binomcxplemnotnn0  40737  sub2times  41589  mul13d  41594  fperiodmullem  41619  fperiodmul  41620  isumneg  41932  climneg  41940  itgsinexp  42289  stoweidlem13  42347  stoweidlem42  42376  wallispilem4  42402  wallispilem5  42403  wallispi2lem1  42405  stirlinglem1  42408  stirlinglem3  42410  stirlinglem4  42411  stirlinglem5  42412  stirlinglem7  42414  stirlinglem10  42417  dirkertrigeqlem3  42434  fourierdlem30  42471  fourierdlem32  42473  fourierdlem42  42483  fourierdlem48  42488  fourierdlem49  42489  fourierdlem83  42523  sqwvfoura  42562  sqwvfourb  42563  etransclem2  42570  etransclem46  42614  sharhght  43171  imasetpreimafvbijlemfv  43611  fmtnorec3  43759  quad1  43834  requad1  43836  isomgreqve  44039  ushrisomgr  44055  rngcid  44299  ringcid  44345  lmodvsmdi  44479  dmatALTbas  44505  ldepsprlem  44576  1subrec1sub  44741  eenglngeehlnmlem1  44773  eenglngeehlnmlem2  44774  itsclc0xyqsolr  44805  sinhpcosh  44888