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 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

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

This theorem is referenced by:  fmptapd  6927  negsub  10928  neg2sub  10940  divmuleq  11339  divneg2  11358  discr  13595  bcpasc  13675  hashgval2  13733  hashf1lem2  13808  relexpaddnn  14404  crim  14468  remullem  14481  isum1p  15190  geo2sum  15223  fallfacfwd  15384  fsumkthpow  15404  bpoly3  15406  bpoly4  15407  efi4p  15484  sinhval  15501  addcos  15521  cos2tsin  15526  demoivreALT  15548  rpnnen2lem11  15571  omeo  15709  pwp1fsum  15736  sadaddlem  15809  bitsres  15816  smumullem  15835  sqgcd  15903  eulerthlem2  16113  vfermltlALT  16133  pockthlem  16235  4sqlem10  16277  vdwlem2  16312  vdwlem6  16316  vdwlem8  16318  fuccocl  17228  resssetc  17346  resscatc  17359  uncfcurf  17483  yonedalem3b  17523  prdspjmhm  17987  grpinvid2  18149  imasgrp2  18208  mulgaddcomlem  18244  mulgmodid  18260  lagsubg2  18335  cntzsubm  18460  sylow3lem2  18747  efgredleme  18863  ablsubsub  18932  ablsubsub4  18933  odadd2  18963  gex2abl  18965  pgpfac1lem3a  19192  abvneg  19599  lmodfopne  19666  lsppr  19859  psrass1  20179  resspsradd  20190  resspsrvsca  20192  mplcoe5  20243  mplmon2mul  20275  evlslem2  20286  evlsvarsrng  20306  coe1tm  20435  ply1scl1  20454  evls1varsrng  20497  gzrngunit  20605  frlmsubgval  20903  frlmgsum  20910  mamuass  21005  mavmulass  21152  mulmarep1gsum2  21177  mdetuni0  21224  maducoeval2  21243  madulid  21248  mat2pmatmul  21333  decpmatmulsumfsupp  21375  pmatcollpwlem  21382  pm2mpmhmlem1  21420  cmpfi  22010  cnconn  22024  txrest  22233  utopsnneiplem  22850  blcvx  23400  tcphcphlem2  23833  cphipval2  23838  cphipval  23840  rrx0  23994  minveclem2  24023  pjthlem1  24034  uniioovol  24174  uniioombllem2  24178  itg1addlem4  24294  mbfi1fseqlem5  24314  itg2mulc  24342  itg2monolem1  24345  itgaddlem1  24417  itgmulc2lem2  24427  dvrec  24546  lhop2  24606  ftc1lem5  24631  deg1submon1p  24740  plypf1  24796  coefv0  24832  coemulhi  24838  coemulc  24839  dgreq0  24849  dvply1  24867  vieta1  24895  aareccl  24909  aaliou3lem8  24928  dvtaylp  24952  mtest  24986  sineq0  25103  efif1olem2  25121  efif1olem4  25123  tanarg  25196  logtayl2  25239  nnlogbexp  25353  isosctrlem2  25391  chordthmlem2  25405  chordthmlem4  25407  heron  25410  dcubic1lem  25415  dcubic1  25417  mcubic  25419  dquart  25425  quart1lem  25427  quart1  25428  efiasin  25460  asinsin  25464  atancj  25482  efiatan  25484  atanlogaddlem  25485  cosatan  25493  atantan  25495  atans2  25503  log2cnv  25516  log2tlbnd  25517  birthdaylem2  25524  cxplim  25543  lgamgulmlem2  25601  wilthlem1  25639  basellem3  25654  musum  25762  musumsum  25763  muinv  25764  pclogsum  25785  mersenne  25797  dchrabs  25830  dchrinv  25831  lgseisenlem1  25945  lgsquadlem1  25950  lgsquadlem2  25951  lgsquadlem3  25952  lgsquad2lem1  25954  2lgslem1  25964  2sqmod  26006  chebbnd1lem3  26041  chpchtlim  26049  rplogsumlem2  26055  dchrisumlem2  26060  dchrmusum2  26064  mulog2sumlem1  26104  mulog2sumlem3  26106  vmalogdivsum2  26108  selberg4lem1  26130  pntrlog2bndlem2  26148  pntrlog2bndlem4  26150  pntibndlem2  26161  pntlemr  26172  pntlemf  26175  pntlemo  26177  ragcom  26478  colperpexlem1  26510  lmiisolem  26576  hypcgrlem2  26580  trgcopyeulem  26585  brbtwn2  26685  colinearalglem1  26686  colinearalglem2  26687  axcontlem2  26745  axcontlem8  26751  numedglnl  26923  clwlkclwwlklem2a  27770  numclwlk1lem1  28142  numclwlk1lem2  28143  numclwwlk2  28154  grpoinvid2  28300  ablodivdiv4  28325  smcnlem  28468  ipidsq  28481  ipasslem2  28603  minvecolem2  28646  hv2times  28832  pjhthlem1  29162  pjds3i  29484  ho2times  29590  opsqrlem6  29916  pjclem4  29970  pj3si  29978  csmdsymi  30105  ofoprabco  30403  fcnvgreu  30412  swrdrndisj  30626  trsp2cyc  30760  cycpmco2lem3  30765  cycpmco2lem4  30766  cycpmco2lem5  30767  cycpmco2lem6  30768  cycpmco2  30770  imaslmod  30917  frlmdim  31004  rrxdim  31007  lbsdiflsp0  31017  fedgmullem1  31020  fedgmullem2  31021  extdg1id  31048  ccfldextdgrr  31052  qqhcn  31227  esumpr2  31321  esumpfinval  31329  esumpfinvalf  31330  carsggect  31571  oddpwdcv  31608  eulerpartlemgs2  31633  fibp1  31654  orvcelval  31721  ballotlemscr  31771  ballotlemfrci  31780  signsplypnf  31815  reprpmtf1o  31892  breprexplemc  31898  breprexp  31899  circlemeth  31906  lpadright  31950  revwlk  32366  subfacp1lem5  32426  cvmliftlem10  32536  circum  32912  faclimlem3  32972  fwddifnp1  33621  bj-bary1lem  34585  tan2h  34878  poimirlem3  34889  poimirlem13  34899  poimirlem14  34900  itgaddnclem1  34944  itgmulc2nclem2  34953  areacirclem1  34976  areacirclem4  34979  istotbnd3  35043  iscringd  35270  3atlem1  36613  pmod2iN  36979  polval2N  37036  lhple  37172  cdleme2  37358  cdleme35d  37582  cdleme42h  37612  cdlemeg46ngfr  37648  cdlemkid1  38052  lcfl7lem  38629  mapdpglem22  38823  mapdh6dN  38869  hdmap1l6d  38943  hdmapinvlem3  39050  nnadddir  39156  expgcd  39176  readdsub  39207  prjspeclsp  39255  3cubeslem3r  39277  diophin  39362  irrapxlem2  39413  pellexlem6  39424  pell1234qrmulcl  39445  rmxyval  39505  rmxyneg  39510  rmxyadd  39511  jm2.24  39553  jm2.25  39589  snhesn  40125  scottrankd  40577  radcnvrat  40639  binomcxplemnotnn0  40681  sub2times  41533  mul13d  41538  fperiodmullem  41563  fperiodmul  41564  isumneg  41876  climneg  41884  itgsinexp  42233  stoweidlem13  42292  stoweidlem42  42321  wallispilem4  42347  wallispilem5  42348  wallispi2lem1  42350  stirlinglem1  42353  stirlinglem3  42355  stirlinglem4  42356  stirlinglem5  42357  stirlinglem7  42359  stirlinglem10  42362  dirkertrigeqlem3  42379  fourierdlem30  42416  fourierdlem32  42418  fourierdlem42  42428  fourierdlem48  42433  fourierdlem49  42434  fourierdlem83  42468  sqwvfoura  42507  sqwvfourb  42508  etransclem2  42515  etransclem46  42559  sharhght  43116  imasetpreimafvbijlemfv  43556  fmtnorec3  43704  quad1  43779  requad1  43781  isomgreqve  43984  ushrisomgr  44000  rngcid  44244  ringcid  44290  lmodvsmdi  44424  dmatALTbas  44450  ldepsprlem  44521  1subrec1sub  44686  eenglngeehlnmlem1  44718  eenglngeehlnmlem2  44719  itsclc0xyqsolr  44750  sinhpcosh  44833