Theorem 3eqtr2d 2776

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

Syntax hints:   → wi 4   = wceq 1539

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  fmptapd  7170  negsub  11512  neg2sub  11524  divmuleq  11923  divneg2  11942  discr  14207  bcpasc  14285  hashgval2  14342  hashf1lem2  14421  relexpaddnn  15002  crim  15066  remullem  15079  isum1p  15791  geo2sum  15823  fallfacfwd  15984  fsumkthpow  16004  bpoly3  16006  bpoly4  16007  efi4p  16084  sinhval  16101  addcos  16121  cos2tsin  16126  demoivreALT  16148  rpnnen2lem11  16171  omeo  16313  pwp1fsum  16338  sadaddlem  16411  bitsres  16418  smumullem  16437  sqgcd  16506  eulerthlem2  16719  vfermltlALT  16739  pockthlem  16842  4sqlem10  16884  vdwlem2  16919  vdwlem6  16923  vdwlem8  16925  fuccocl  17921  resssetc  18046  resscatc  18063  uncfcurf  18196  yonedalem3b  18236  prdspjmhm  18746  grpinvid2  18913  imasgrp2  18974  mulgaddcomlem  19013  mulgmodid  19029  lagsubg2  19109  cntzsgrpcl  19239  cntzsubm  19243  sylow3lem2  19537  efgredleme  19652  ablsubsub  19726  ablsubsub4  19727  odadd2  19758  gex2abl  19760  pgpfac1lem3a  19987  pwspjmhmmgpd  20216  abvneg  20585  lmodfopne  20654  lsppr  20848  rngqiprngfulem4  21073  gzrngunit  21211  frlmsubgval  21539  frlmgsum  21546  psrass1  21744  resspsradd  21755  resspsrvsca  21757  mplcoe5  21814  mplmon2mul  21849  evlslem2  21861  evlsvarsrng  21881  coe1tm  22015  ply1scl1OLD  22036  evls1varsrng  22079  mamuass  22122  mavmulass  22271  mulmarep1gsum2  22296  mdetuni0  22343  maducoeval2  22362  madulid  22367  mat2pmatmul  22453  decpmatmulsumfsupp  22495  pmatcollpwlem  22502  pm2mpmhmlem1  22540  cmpfi  23132  cnconn  23146  txrest  23355  utopsnneiplem  23972  blcvx  24534  tcphcphlem2  24984  cphipval2  24989  cphipval  24991  rrx0  25145  minveclem2  25174  pjthlem1  25185  uniioovol  25328  uniioombllem2  25332  itg1addlem4  25448  itg1addlem4OLD  25449  mbfi1fseqlem5  25469  itg2mulc  25497  itg2monolem1  25500  itgaddlem1  25572  itgmulc2lem2  25582  dvrec  25707  lhop2  25767  ftc1lem5  25792  deg1submon1p  25905  plypf1  25961  coefv0  25997  coemulhi  26003  coemulc  26004  dgreq0  26015  dvply1  26033  vieta1  26061  aareccl  26075  aaliou3lem8  26094  dvtaylp  26118  mtest  26152  sineq0  26269  efif1olem2  26288  efif1olem4  26290  tanarg  26363  logtayl2  26406  nnlogbexp  26522  isosctrlem2  26560  chordthmlem2  26574  chordthmlem4  26576  heron  26579  dcubic1lem  26584  dcubic1  26586  mcubic  26588  dquart  26594  quart1lem  26596  quart1  26597  efiasin  26629  asinsin  26633  atancj  26651  efiatan  26653  atanlogaddlem  26654  cosatan  26662  atantan  26664  atans2  26672  log2cnv  26685  log2tlbnd  26686  birthdaylem2  26693  cxplim  26712  lgamgulmlem2  26770  wilthlem1  26808  basellem3  26823  musum  26931  musumsum  26932  muinv  26933  pclogsum  26954  mersenne  26966  dchrabs  26999  dchrinv  27000  lgseisenlem1  27114  lgsquadlem1  27119  lgsquadlem2  27120  lgsquadlem3  27121  lgsquad2lem1  27123  2lgslem1  27133  2sqmod  27175  chebbnd1lem3  27210  chpchtlim  27218  rplogsumlem2  27224  dchrisumlem2  27229  dchrmusum2  27233  mulog2sumlem1  27273  mulog2sumlem3  27275  vmalogdivsum2  27277  selberg4lem1  27299  pntrlog2bndlem2  27317  pntrlog2bndlem4  27319  pntibndlem2  27330  pntlemr  27341  pntlemf  27344  pntlemo  27346  addsdilem4  27848  ragcom  28216  colperpexlem1  28248  lmiisolem  28314  hypcgrlem2  28318  trgcopyeulem  28323  brbtwn2  28430  colinearalglem1  28431  colinearalglem2  28432  axcontlem2  28490  axcontlem8  28496  numedglnl  28671  clwlkclwwlklem2a  29518  numclwlk1lem1  29889  numclwlk1lem2  29890  numclwwlk2  29901  grpoinvid2  30049  ablodivdiv4  30074  smcnlem  30217  ipidsq  30230  ipasslem2  30352  minvecolem2  30395  hv2times  30581  pjhthlem1  30911  pjds3i  31233  ho2times  31339  opsqrlem6  31665  pjclem4  31719  pj3si  31727  csmdsymi  31854  ofoprabco  32156  fcnvgreu  32165  swrdrndisj  32388  trsp2cyc  32552  cycpmco2lem3  32557  cycpmco2lem4  32558  cycpmco2lem5  32559  cycpmco2lem6  32560  cycpmco2  32562  imaslmod  32738  ply1fermltlchr  32936  r1padd1  32953  frlmdim  32984  rrxdim  32987  lbsdiflsp0  32999  fedgmullem1  33002  fedgmullem2  33003  extdg1id  33030  ccfldextdgrr  33035  qqhcn  33269  esumpr2  33363  esumpfinval  33371  esumpfinvalf  33372  carsggect  33615  oddpwdcv  33652  eulerpartlemgs2  33677  fibp1  33698  orvcelval  33765  ballotlemscr  33815  ballotlemfrci  33824  signsplypnf  33859  reprpmtf1o  33936  breprexplemc  33942  breprexp  33943  circlemeth  33950  lpadright  33994  revwlk  34413  subfacp1lem5  34473  cvmliftlem10  34583  circum  34957  faclimlem3  35019  fwddifnp1  35441  bj-bary1lem  36494  tan2h  36783  poimirlem3  36794  poimirlem13  36804  poimirlem14  36805  itgaddnclem1  36849  itgmulc2nclem2  36858  areacirclem1  36879  areacirclem4  36882  istotbnd3  36942  iscringd  37169  3atlem1  38657  pmod2iN  39023  polval2N  39080  lhple  39216  cdleme2  39402  cdleme35d  39626  cdleme42h  39656  cdlemeg46ngfr  39692  cdlemkid1  40096  lcfl7lem  40673  mapdpglem22  40867  mapdh6dN  40913  hdmap1l6d  40987  hdmapinvlem3  41094  lcmineqlem3  41202  selvvvval  41459  evlselv  41461  evlsmhpvvval  41469  nnadddir  41486  expgcd  41527  readdsub  41559  sn-negex12  41591  zmulcomlem  41630  prjspeclsp  41656  prjspner1  41670  3cubeslem3r  41727  diophin  41812  irrapxlem2  41863  pellexlem6  41874  pell1234qrmulcl  41895  rmxyval  41956  rmxyneg  41961  rmxyadd  41962  jm2.24  42004  jm2.25  42040  limexissupab  42335  omabs2  42384  tfsconcatrev  42400  naddwordnexlem4  42454  snhesn  42839  scottrankd  43309  radcnvrat  43375  binomcxplemnotnn0  43417  sub2times  44280  mul13d  44287  fperiodmullem  44311  fperiodmul  44312  isumneg  44616  climneg  44624  itgsinexp  44969  stoweidlem13  45027  stoweidlem42  45056  wallispilem4  45082  wallispilem5  45083  wallispi2lem1  45085  stirlinglem1  45088  stirlinglem3  45090  stirlinglem4  45091  stirlinglem5  45092  stirlinglem7  45094  stirlinglem10  45097  dirkertrigeqlem3  45114  fourierdlem30  45151  fourierdlem32  45153  fourierdlem42  45163  fourierdlem48  45168  fourierdlem49  45169  fourierdlem83  45203  sqwvfoura  45242  sqwvfourb  45243  etransclem2  45250  etransclem46  45294  sharhght  45879  imasetpreimafvbijlemfv  46368  fmtnorec3  46514  quad1  46586  requad1  46588  isomgreqve  46791  ushrisomgr  46807  rngcid  46965  ringcid  47011  lmodvsmdi  47146  dmatALTbas  47169  ldepsprlem  47240  itcovalt2lem2lem2  47447  ackval3  47456  1subrec1sub  47478  eenglngeehlnmlem1  47510  eenglngeehlnmlem2  47511  itsclc0xyqsolr  47542  sinhpcosh  47872