Theorem 3eqtr2d 2780

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

Syntax hints:   → wi 4   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  fmptapd  7190  negsub  11554  neg2sub  11566  divmuleq  11969  divneg2  11988  discr  14275  bcpasc  14356  hashgval2  14413  hashf1lem2  14491  relexpaddnn  15086  crim  15150  remullem  15163  isum1p  15873  geo2sum  15905  fallfacfwd  16068  fsumkthpow  16088  bpoly3  16090  bpoly4  16091  efi4p  16169  sinhval  16186  addcos  16206  cos2tsin  16211  demoivreALT  16233  rpnnen2lem11  16256  omeo  16399  pwp1fsum  16424  sadaddlem  16499  bitsres  16506  smumullem  16525  sqgcd  16595  expgcd  16596  eulerthlem2  16815  vfermltlALT  16835  pockthlem  16938  4sqlem10  16980  vdwlem2  17015  vdwlem6  17019  vdwlem8  17021  fuccocl  18020  resssetc  18145  resscatc  18162  uncfcurf  18295  yonedalem3b  18335  prdspjmhm  18854  grpinvid2  19022  imasgrp2  19085  mulgaddcomlem  19127  mulgmodid  19143  lagsubg2  19224  cntzsgrpcl  19364  cntzsubm  19368  sylow3lem2  19660  efgredleme  19775  ablsubsub  19849  ablsubsub4  19850  odadd2  19881  gex2abl  19883  pgpfac1lem3a  20110  pwspjmhmmgpd  20341  rngcid  20651  ringcid  20680  abvneg  20843  lmodfopne  20914  lsppr  21109  rngqiprngfulem4  21341  gzrngunit  21468  frlmsubgval  21802  frlmgsum  21809  psrass1  22001  resspsradd  22012  resspsrvsca  22014  mplcoe5  22075  mplmon2mul  22110  evlslem2  22120  evlsvarsrng  22140  coe1tm  22291  ply1scl1OLD  22312  ply1fermltlchr  22331  evls1varsrng  22359  mamuass  22421  mavmulass  22570  mulmarep1gsum2  22595  mdetuni0  22642  maducoeval2  22661  madulid  22666  mat2pmatmul  22752  decpmatmulsumfsupp  22794  pmatcollpwlem  22801  pm2mpmhmlem1  22839  cmpfi  23431  cnconn  23445  txrest  23654  utopsnneiplem  24271  blcvx  24833  tcphcphlem2  25283  cphipval2  25288  cphipval  25290  rrx0  25444  minveclem2  25473  pjthlem1  25484  uniioovol  25627  uniioombllem2  25631  itg1addlem4  25747  itg1addlem4OLD  25748  mbfi1fseqlem5  25768  itg2mulc  25796  itg2monolem1  25799  itgaddlem1  25872  itgmulc2lem2  25882  dvrec  26007  lhop2  26068  ftc1lem5  26095  deg1submon1p  26206  plypf1  26265  coefv0  26301  coemulhi  26307  coemulc  26308  dgreq0  26319  dvply1  26339  vieta1  26368  aareccl  26382  aaliou3lem8  26401  dvtaylp  26426  mtest  26461  sineq0  26580  efif1olem2  26599  efif1olem4  26601  tanarg  26675  logtayl2  26718  nnlogbexp  26838  isosctrlem2  26876  chordthmlem2  26890  chordthmlem4  26892  heron  26895  dcubic1lem  26900  dcubic1  26902  mcubic  26904  dquart  26910  quart1lem  26912  quart1  26913  efiasin  26945  asinsin  26949  atancj  26967  efiatan  26969  atanlogaddlem  26970  cosatan  26978  atantan  26980  atans2  26988  log2cnv  27001  log2tlbnd  27002  birthdaylem2  27009  cxplim  27029  lgamgulmlem2  27087  wilthlem1  27125  basellem3  27140  musum  27248  musumsum  27249  muinv  27250  pclogsum  27273  mersenne  27285  dchrabs  27318  dchrinv  27319  lgseisenlem1  27433  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  lgsquad2lem1  27442  2lgslem1  27452  2sqmod  27494  chebbnd1lem3  27529  chpchtlim  27537  rplogsumlem2  27543  dchrisumlem2  27548  dchrmusum2  27552  mulog2sumlem1  27592  mulog2sumlem3  27594  vmalogdivsum2  27596  selberg4lem1  27618  pntrlog2bndlem2  27636  pntrlog2bndlem4  27638  pntibndlem2  27649  pntlemr  27660  pntlemf  27663  pntlemo  27665  addsdilem4  28194  mulsunif2lem  28209  halfcut  28430  zs12bday  28438  ragcom  28720  colperpexlem1  28752  lmiisolem  28818  hypcgrlem2  28822  trgcopyeulem  28827  brbtwn2  28934  colinearalglem1  28935  colinearalglem2  28936  axcontlem2  28994  axcontlem8  29000  numedglnl  29175  clwlkclwwlklem2a  30026  numclwlk1lem1  30397  numclwlk1lem2  30398  numclwwlk2  30409  grpoinvid2  30557  ablodivdiv4  30582  smcnlem  30725  ipidsq  30738  ipasslem2  30860  minvecolem2  30903  hv2times  31089  pjhthlem1  31419  pjds3i  31741  ho2times  31847  opsqrlem6  32173  pjclem4  32227  pj3si  32235  csmdsymi  32362  ofoprabco  32680  fcnvgreu  32689  quad3d  32760  swrdrndisj  32926  trsp2cyc  33125  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2  33135  elrgspnlem1  33231  rlocmulval  33255  imaslmod  33360  1arithufdlem3  33553  r1padd1  33607  frlmdim  33638  rrxdim  33641  lbsdiflsp0  33653  fedgmullem1  33656  fedgmullem2  33657  extdg1id  33690  ccfldextdgrr  33696  constrrtlc1  33737  constrrtcclem  33739  constrrtcc  33740  qqhcn  33953  esumpr2  34047  esumpfinval  34055  esumpfinvalf  34056  carsggect  34299  oddpwdcv  34336  eulerpartlemgs2  34361  fibp1  34382  orvcelval  34449  ballotlemscr  34499  ballotlemfrci  34508  signsplypnf  34543  reprpmtf1o  34619  breprexplemc  34625  breprexp  34626  circlemeth  34633  lpadright  34677  revwlk  35108  subfacp1lem5  35168  cvmliftlem10  35278  circum  35658  faclimlem3  35724  fwddifnp1  36146  bj-bary1lem  37292  tan2h  37598  poimirlem3  37609  poimirlem13  37619  poimirlem14  37620  itgaddnclem1  37664  itgmulc2nclem2  37673  areacirclem1  37694  areacirclem4  37697  istotbnd3  37757  iscringd  37984  3atlem1  39465  pmod2iN  39831  polval2N  39888  lhple  40024  cdleme2  40210  cdleme35d  40434  cdleme42h  40464  cdlemeg46ngfr  40500  cdlemkid1  40904  lcfl7lem  41481  mapdpglem22  41675  mapdh6dN  41721  hdmap1l6d  41795  hdmapinvlem3  41902  lcmineqlem3  42012  nnadddir  42283  readvrec2  42369  readdsub  42390  sn-negex12  42422  zmulcomlem  42461  selvvvval  42571  evlselv  42573  evlsmhpvvval  42581  prjspeclsp  42598  prjspner1  42612  3cubeslem3r  42674  diophin  42759  irrapxlem2  42810  pellexlem6  42821  pell1234qrmulcl  42842  rmxyval  42903  rmxyneg  42908  rmxyadd  42909  jm2.24  42951  jm2.25  42987  limexissupab  43272  omabs2  43321  tfsconcatrev  43337  naddwordnexlem4  43390  snhesn  43775  scottrankd  44243  radcnvrat  44309  binomcxplemnotnn0  44351  sub2times  45222  mul13d  45229  fperiodmullem  45253  fperiodmul  45254  isumneg  45557  climneg  45565  itgsinexp  45910  stoweidlem13  45968  stoweidlem42  45997  wallispilem4  46023  wallispilem5  46024  wallispi2lem1  46026  stirlinglem1  46029  stirlinglem3  46031  stirlinglem4  46032  stirlinglem5  46033  stirlinglem7  46035  stirlinglem10  46038  dirkertrigeqlem3  46055  fourierdlem30  46092  fourierdlem32  46094  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem83  46144  sqwvfoura  46183  sqwvfourb  46184  etransclem2  46191  etransclem46  46235  sharhght  46820  imasetpreimafvbijlemfv  47326  fmtnorec3  47472  quad1  47544  requad1  47546  ushggricedg  47833  lmodvsmdi  48223  dmatALTbas  48246  ldepsprlem  48317  itcovalt2lem2lem2  48523  ackval3  48532  1subrec1sub  48554  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  itsclc0xyqsolr  48618  sinhpcosh  48970