Theorem 3eqtr2d 2783

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

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

This theorem is referenced by:  fmptapd  7191  negsub  11557  neg2sub  11569  divmuleq  11972  divneg2  11991  discr  14279  bcpasc  14360  hashgval2  14417  hashf1lem2  14495  relexpaddnn  15090  crim  15154  remullem  15167  isum1p  15877  geo2sum  15909  fallfacfwd  16072  fsumkthpow  16092  bpoly3  16094  bpoly4  16095  efi4p  16173  sinhval  16190  addcos  16210  cos2tsin  16215  demoivreALT  16237  rpnnen2lem11  16260  omeo  16403  pwp1fsum  16428  sadaddlem  16503  bitsres  16510  smumullem  16529  sqgcd  16599  expgcd  16600  eulerthlem2  16819  vfermltlALT  16840  pockthlem  16943  4sqlem10  16985  vdwlem2  17020  vdwlem6  17024  vdwlem8  17026  fuccocl  18012  resssetc  18137  resscatc  18154  uncfcurf  18284  yonedalem3b  18324  prdspjmhm  18842  grpinvid2  19010  imasgrp2  19073  mulgaddcomlem  19115  mulgmodid  19131  lagsubg2  19212  cntzsgrpcl  19352  cntzsubm  19356  sylow3lem2  19646  efgredleme  19761  ablsubsub  19835  ablsubsub4  19836  odadd2  19867  gex2abl  19869  pgpfac1lem3a  20096  pwspjmhmmgpd  20325  rngcid  20635  ringcid  20664  abvneg  20827  lmodfopne  20898  lsppr  21092  rngqiprngfulem4  21324  gzrngunit  21451  frlmsubgval  21785  frlmgsum  21792  psrass1  21984  resspsradd  21995  resspsrvsca  21997  mplcoe5  22058  mplmon2mul  22093  evlslem2  22103  evlsvarsrng  22123  coe1tm  22276  ply1scl1OLD  22297  ply1fermltlchr  22316  evls1varsrng  22344  mamuass  22406  mavmulass  22555  mulmarep1gsum2  22580  mdetuni0  22627  maducoeval2  22646  madulid  22651  mat2pmatmul  22737  decpmatmulsumfsupp  22779  pmatcollpwlem  22786  pm2mpmhmlem1  22824  cmpfi  23416  cnconn  23430  txrest  23639  utopsnneiplem  24256  blcvx  24819  tcphcphlem2  25270  cphipval2  25275  cphipval  25277  rrx0  25431  minveclem2  25460  pjthlem1  25471  uniioovol  25614  uniioombllem2  25618  itg1addlem4  25734  mbfi1fseqlem5  25754  itg2mulc  25782  itg2monolem1  25785  itgaddlem1  25858  itgmulc2lem2  25868  dvrec  25993  lhop2  26054  ftc1lem5  26081  deg1submon1p  26192  plypf1  26251  coefv0  26287  coemulhi  26293  coemulc  26294  dgreq0  26305  dvply1  26325  vieta1  26354  aareccl  26368  aaliou3lem8  26387  dvtaylp  26412  mtest  26447  sineq0  26566  efif1olem2  26585  efif1olem4  26587  tanarg  26661  logtayl2  26704  nnlogbexp  26824  isosctrlem2  26862  chordthmlem2  26876  chordthmlem4  26878  heron  26881  dcubic1lem  26886  dcubic1  26888  mcubic  26890  dquart  26896  quart1lem  26898  quart1  26899  efiasin  26931  asinsin  26935  atancj  26953  efiatan  26955  atanlogaddlem  26956  cosatan  26964  atantan  26966  atans2  26974  log2cnv  26987  log2tlbnd  26988  birthdaylem2  26995  cxplim  27015  lgamgulmlem2  27073  wilthlem1  27111  basellem3  27126  musum  27234  musumsum  27235  muinv  27236  pclogsum  27259  mersenne  27271  dchrabs  27304  dchrinv  27305  lgseisenlem1  27419  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  lgsquad2lem1  27428  2lgslem1  27438  2sqmod  27480  chebbnd1lem3  27515  chpchtlim  27523  rplogsumlem2  27529  dchrisumlem2  27534  dchrmusum2  27538  mulog2sumlem1  27578  mulog2sumlem3  27580  vmalogdivsum2  27582  selberg4lem1  27604  pntrlog2bndlem2  27622  pntrlog2bndlem4  27624  pntibndlem2  27635  pntlemr  27646  pntlemf  27649  pntlemo  27651  addsdilem4  28180  mulsunif2lem  28195  halfcut  28416  zs12bday  28424  ragcom  28706  colperpexlem1  28738  lmiisolem  28804  hypcgrlem2  28808  trgcopyeulem  28813  brbtwn2  28920  colinearalglem1  28921  colinearalglem2  28922  axcontlem2  28980  axcontlem8  28986  numedglnl  29161  clwlkclwwlklem2a  30017  numclwlk1lem1  30388  numclwlk1lem2  30389  numclwwlk2  30400  grpoinvid2  30548  ablodivdiv4  30573  smcnlem  30716  ipidsq  30729  ipasslem2  30851  minvecolem2  30894  hv2times  31080  pjhthlem1  31410  pjds3i  31732  ho2times  31838  opsqrlem6  32164  pjclem4  32218  pj3si  32226  csmdsymi  32353  ofoprabco  32674  fcnvgreu  32683  quad3d  32754  swrdrndisj  32942  trsp2cyc  33143  cycpmco2lem3  33148  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2  33153  elrgspnlem1  33246  rlocmulval  33273  imaslmod  33381  1arithufdlem3  33574  r1padd1  33628  frlmdim  33662  rrxdim  33665  lbsdiflsp0  33677  fedgmullem1  33680  fedgmullem2  33681  extdg1id  33716  ccfldextdgrr  33722  fldextrspunlem1  33725  constrrtlc1  33773  constrrtcclem  33775  constrrtcc  33776  qqhcn  33992  esumpr2  34068  esumpfinval  34076  esumpfinvalf  34077  carsggect  34320  oddpwdcv  34357  eulerpartlemgs2  34382  fibp1  34403  orvcelval  34471  ballotlemscr  34521  ballotlemfrci  34530  signsplypnf  34565  reprpmtf1o  34641  breprexplemc  34647  breprexp  34648  circlemeth  34655  lpadright  34699  revwlk  35130  subfacp1lem5  35189  cvmliftlem10  35299  circum  35679  faclimlem3  35745  fwddifnp1  36166  bj-bary1lem  37311  tan2h  37619  poimirlem3  37630  poimirlem13  37640  poimirlem14  37641  itgaddnclem1  37685  itgmulc2nclem2  37694  areacirclem1  37715  areacirclem4  37718  istotbnd3  37778  iscringd  38005  3atlem1  39485  pmod2iN  39851  polval2N  39908  lhple  40044  cdleme2  40230  cdleme35d  40454  cdleme42h  40484  cdlemeg46ngfr  40520  cdlemkid1  40924  lcfl7lem  41501  mapdpglem22  41695  mapdh6dN  41741  hdmap1l6d  41815  hdmapinvlem3  41922  lcmineqlem3  42032  nnadddir  42305  readvrec2  42391  readdsub  42414  sn-negex12  42446  zmulcomlem  42485  selvvvval  42595  evlselv  42597  evlsmhpvvval  42605  prjspeclsp  42622  prjspner1  42636  3cubeslem3r  42698  diophin  42783  irrapxlem2  42834  pellexlem6  42845  pell1234qrmulcl  42866  rmxyval  42927  rmxyneg  42932  rmxyadd  42933  jm2.24  42975  jm2.25  43011  limexissupab  43296  omabs2  43345  tfsconcatrev  43361  naddwordnexlem4  43414  snhesn  43799  scottrankd  44267  radcnvrat  44333  binomcxplemnotnn0  44375  sub2times  45284  mul13d  45291  fperiodmullem  45315  fperiodmul  45316  isumneg  45617  climneg  45625  itgsinexp  45970  stoweidlem13  46028  stoweidlem42  46057  wallispilem4  46083  wallispilem5  46084  wallispi2lem1  46086  stirlinglem1  46089  stirlinglem3  46091  stirlinglem4  46092  stirlinglem5  46093  stirlinglem7  46095  stirlinglem10  46098  dirkertrigeqlem3  46115  fourierdlem30  46152  fourierdlem32  46154  fourierdlem42  46164  fourierdlem48  46169  fourierdlem49  46170  fourierdlem83  46204  sqwvfoura  46243  sqwvfourb  46244  etransclem2  46251  etransclem46  46295  sharhght  46880  imasetpreimafvbijlemfv  47389  fmtnorec3  47535  quad1  47607  requad1  47609  ushggricedg  47896  lmodvsmdi  48295  dmatALTbas  48318  ldepsprlem  48389  itcovalt2lem2lem2  48595  ackval3  48604  1subrec1sub  48626  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  itsclc0xyqsolr  48690  swapfid  48985  sinhpcosh  49259