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  7127  negsub  11441  neg2sub  11453  divmuleq  11858  divneg2  11877  discr  14175  bcpasc  14256  hashgval2  14313  hashf1lem2  14391  relexpaddnn  14986  crim  15050  remullem  15063  isum1p  15776  geo2sum  15808  fallfacfwd  15971  fsumkthpow  15991  bpoly3  15993  bpoly4  15994  efi4p  16074  sinhval  16091  addcos  16111  cos2tsin  16116  demoivreALT  16138  rpnnen2lem11  16161  omeo  16305  pwp1fsum  16330  sadaddlem  16405  bitsres  16412  smumullem  16431  sqgcd  16501  expgcd  16502  eulerthlem2  16721  vfermltlALT  16742  pockthlem  16845  4sqlem10  16887  vdwlem2  16922  vdwlem6  16926  vdwlem8  16928  fuccocl  17903  resssetc  18028  resscatc  18045  uncfcurf  18174  yonedalem3b  18214  prdspjmhm  18766  grpinvid2  18934  imasgrp2  18997  mulgaddcomlem  19039  mulgmodid  19055  lagsubg2  19135  cntzsgrpcl  19275  cntzsubm  19279  sylow3lem2  19569  efgredleme  19684  ablsubsub  19758  ablsubsub4  19759  odadd2  19790  gex2abl  19792  pgpfac1lem3a  20019  pwspjmhmmgpd  20275  rngcid  20580  ringcid  20609  abvneg  20771  lmodfopne  20863  lsppr  21057  rngqiprngfulem4  21281  gzrngunit  21400  frlmsubgval  21732  frlmgsum  21739  psrass1  21931  resspsradd  21942  resspsrvsca  21944  mplcoe5  22007  mplmon2mul  22036  evlslem2  22046  evlsvarsrng  22074  coe1tm  22227  ply1scl1OLD  22248  ply1fermltlchr  22268  evls1varsrng  22296  mamuass  22358  mavmulass  22505  mulmarep1gsum2  22530  mdetuni0  22577  maducoeval2  22596  madulid  22601  mat2pmatmul  22687  decpmatmulsumfsupp  22729  pmatcollpwlem  22736  pm2mpmhmlem1  22774  cmpfi  23364  cnconn  23378  txrest  23587  utopsnneiplem  24203  blcvx  24754  tcphcphlem2  25204  cphipval2  25209  cphipval  25211  rrx0  25365  minveclem2  25394  pjthlem1  25405  uniioovol  25548  uniioombllem2  25552  itg1addlem4  25668  mbfi1fseqlem5  25688  itg2mulc  25716  itg2monolem1  25719  itgaddlem1  25792  itgmulc2lem2  25802  dvrec  25927  lhop2  25988  ftc1lem5  26015  deg1submon1p  26126  plypf1  26185  coefv0  26221  coemulhi  26227  coemulc  26228  dgreq0  26239  dvply1  26259  vieta1  26288  aareccl  26302  aaliou3lem8  26321  dvtaylp  26346  mtest  26381  sineq0  26501  efif1olem2  26520  efif1olem4  26522  tanarg  26596  logtayl2  26639  nnlogbexp  26759  isosctrlem2  26797  chordthmlem2  26811  chordthmlem4  26813  heron  26816  dcubic1lem  26821  dcubic1  26823  mcubic  26825  dquart  26831  quart1lem  26833  quart1  26834  efiasin  26866  asinsin  26870  atancj  26888  efiatan  26890  atanlogaddlem  26891  cosatan  26899  atantan  26901  atans2  26909  log2cnv  26922  log2tlbnd  26923  birthdaylem2  26930  cxplim  26950  lgamgulmlem2  27008  wilthlem1  27046  basellem3  27061  musum  27169  musumsum  27170  muinv  27171  pclogsum  27194  mersenne  27206  dchrabs  27239  dchrinv  27240  lgseisenlem1  27354  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  lgsquad2lem1  27363  2lgslem1  27373  2sqmod  27415  chebbnd1lem3  27450  chpchtlim  27458  rplogsumlem2  27464  dchrisumlem2  27469  dchrmusum2  27473  mulog2sumlem1  27513  mulog2sumlem3  27515  vmalogdivsum2  27517  selberg4lem1  27539  pntrlog2bndlem2  27557  pntrlog2bndlem4  27559  pntibndlem2  27570  pntlemr  27581  pntlemf  27584  pntlemo  27586  addsdilem4  28162  mulsunif2lem  28177  halfcut  28466  bdayfinbndlem1  28475  ragcom  28782  colperpexlem1  28814  lmiisolem  28880  hypcgrlem2  28884  trgcopyeulem  28889  brbtwn2  28990  colinearalglem1  28991  colinearalglem2  28992  axcontlem2  29050  axcontlem8  29056  numedglnl  29229  clwlkclwwlklem2a  30085  numclwlk1lem1  30456  numclwlk1lem2  30457  numclwwlk2  30468  grpoinvid2  30616  ablodivdiv4  30641  smcnlem  30784  ipidsq  30797  ipasslem2  30919  minvecolem2  30962  hv2times  31148  pjhthlem1  31478  pjds3i  31800  ho2times  31906  opsqrlem6  32232  pjclem4  32286  pj3si  32294  csmdsymi  32421  ofoprabco  32753  fcnvgreu  32761  quad3d  32839  nn0diffz0  32884  swrdrndisj  33049  trsp2cyc  33216  cycpmco2lem3  33221  cycpmco2lem4  33222  cycpmco2lem5  33223  cycpmco2lem6  33224  cycpmco2  33226  conjga  33263  elrgspnlem1  33335  rlocmulval  33362  imaslmod  33445  1arithufdlem3  33638  deg1prod  33675  r1padd1  33700  mplvrpmrhm  33723  esplyfvaln  33750  frlmdim  33788  rrxdim  33791  lbsdiflsp0  33803  fedgmullem1  33806  fedgmullem2  33807  extdg1id  33843  ccfldextdgrr  33849  fldextrspunlem1  33852  constrrtlc1  33909  constrrtcclem  33911  constrrtcc  33912  constrrecl  33946  constrresqrtcl  33954  cos9thpiminplylem1  33959  cos9thpiminplylem2  33960  cos9thpiminplylem3  33961  cos9thpiminply  33965  qqhcn  34168  esumpr2  34244  esumpfinval  34252  esumpfinvalf  34253  carsggect  34495  oddpwdcv  34532  eulerpartlemgs2  34557  fibp1  34578  orvcelval  34646  ballotlemscr  34696  ballotlemfrci  34705  signsplypnf  34727  reprpmtf1o  34803  breprexplemc  34809  breprexp  34810  circlemeth  34817  lpadright  34861  revwlk  35338  subfacp1lem5  35397  cvmliftlem10  35507  circum  35887  faclimlem3  35958  fwddifnp1  36378  bj-bary1lem  37562  tan2h  37860  poimirlem3  37871  poimirlem13  37881  poimirlem14  37882  itgaddnclem1  37926  itgmulc2nclem2  37935  areacirclem1  37956  areacirclem4  37959  istotbnd3  38019  iscringd  38246  3atlem1  39856  pmod2iN  40222  polval2N  40279  lhple  40415  cdleme2  40601  cdleme35d  40825  cdleme42h  40855  cdlemeg46ngfr  40891  cdlemkid1  41295  lcfl7lem  41872  mapdpglem22  42066  mapdh6dN  42112  hdmap1l6d  42186  hdmapinvlem3  42293  lcmineqlem3  42398  nnadddir  42637  readvrec2  42728  readdsub  42751  sn-negex12  42784  zmulcomlem  42834  selvvvval  42940  evlselv  42942  evlsmhpvvval  42950  prjspeclsp  42967  prjspner1  42981  3cubeslem3r  43041  diophin  43126  irrapxlem2  43177  pellexlem6  43188  pell1234qrmulcl  43209  rmxyval  43269  rmxyneg  43274  rmxyadd  43275  jm2.24  43317  jm2.25  43353  limexissupab  43637  omabs2  43686  tfsconcatrev  43702  naddwordnexlem4  43755  snhesn  44139  scottrankd  44601  radcnvrat  44667  binomcxplemnotnn0  44709  sub2times  45632  mul13d  45639  fperiodmullem  45662  fperiodmul  45663  isumneg  45959  climneg  45967  itgsinexp  46310  stoweidlem13  46368  stoweidlem42  46397  wallispilem4  46423  wallispilem5  46424  wallispi2lem1  46426  stirlinglem1  46429  stirlinglem3  46431  stirlinglem4  46432  stirlinglem5  46433  stirlinglem7  46435  stirlinglem10  46438  dirkertrigeqlem3  46455  fourierdlem30  46492  fourierdlem32  46494  fourierdlem42  46504  fourierdlem48  46509  fourierdlem49  46510  fourierdlem83  46544  sqwvfoura  46583  sqwvfourb  46584  etransclem2  46591  etransclem46  46635  sharhght  47220  imasetpreimafvbijlemfv  47759  fmtnorec3  47905  quad1  47977  requad1  47979  ushggricedg  48284  lmodvsmdi  48736  dmatALTbas  48758  ldepsprlem  48829  itcovalt2lem2lem2  49031  ackval3  49040  1subrec1sub  49062  eenglngeehlnmlem1  49094  eenglngeehlnmlem2  49095  itsclc0xyqsolr  49126  swapfid  49635  sinhpcosh  50096