Theorem 3eqtr2d 2770

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 2767	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtrd 2764	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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  fmptapd  7127  negsub  11446  neg2sub  11458  divmuleq  11863  divneg2  11882  discr  14181  bcpasc  14262  hashgval2  14319  hashf1lem2  14397  relexpaddnn  14993  crim  15057  remullem  15070  isum1p  15783  geo2sum  15815  fallfacfwd  15978  fsumkthpow  15998  bpoly3  16000  bpoly4  16001  efi4p  16081  sinhval  16098  addcos  16118  cos2tsin  16123  demoivreALT  16145  rpnnen2lem11  16168  omeo  16312  pwp1fsum  16337  sadaddlem  16412  bitsres  16419  smumullem  16438  sqgcd  16508  expgcd  16509  eulerthlem2  16728  vfermltlALT  16749  pockthlem  16852  4sqlem10  16894  vdwlem2  16929  vdwlem6  16933  vdwlem8  16935  fuccocl  17905  resssetc  18030  resscatc  18047  uncfcurf  18176  yonedalem3b  18216  prdspjmhm  18732  grpinvid2  18900  imasgrp2  18963  mulgaddcomlem  19005  mulgmodid  19021  lagsubg2  19102  cntzsgrpcl  19242  cntzsubm  19246  sylow3lem2  19534  efgredleme  19649  ablsubsub  19723  ablsubsub4  19724  odadd2  19755  gex2abl  19757  pgpfac1lem3a  19984  pwspjmhmmgpd  20213  rngcid  20520  ringcid  20549  abvneg  20711  lmodfopne  20782  lsppr  20976  rngqiprngfulem4  21200  gzrngunit  21326  frlmsubgval  21650  frlmgsum  21657  psrass1  21849  resspsradd  21860  resspsrvsca  21862  mplcoe5  21923  mplmon2mul  21952  evlslem2  21962  evlsvarsrng  21982  coe1tm  22135  ply1scl1OLD  22156  ply1fermltlchr  22175  evls1varsrng  22203  mamuass  22265  mavmulass  22412  mulmarep1gsum2  22437  mdetuni0  22484  maducoeval2  22503  madulid  22508  mat2pmatmul  22594  decpmatmulsumfsupp  22636  pmatcollpwlem  22643  pm2mpmhmlem1  22681  cmpfi  23271  cnconn  23285  txrest  23494  utopsnneiplem  24111  blcvx  24662  tcphcphlem2  25112  cphipval2  25117  cphipval  25119  rrx0  25273  minveclem2  25302  pjthlem1  25313  uniioovol  25456  uniioombllem2  25460  itg1addlem4  25576  mbfi1fseqlem5  25596  itg2mulc  25624  itg2monolem1  25627  itgaddlem1  25700  itgmulc2lem2  25710  dvrec  25835  lhop2  25896  ftc1lem5  25923  deg1submon1p  26034  plypf1  26093  coefv0  26129  coemulhi  26135  coemulc  26136  dgreq0  26147  dvply1  26167  vieta1  26196  aareccl  26210  aaliou3lem8  26229  dvtaylp  26254  mtest  26289  sineq0  26409  efif1olem2  26428  efif1olem4  26430  tanarg  26504  logtayl2  26547  nnlogbexp  26667  isosctrlem2  26705  chordthmlem2  26719  chordthmlem4  26721  heron  26724  dcubic1lem  26729  dcubic1  26731  mcubic  26733  dquart  26739  quart1lem  26741  quart1  26742  efiasin  26774  asinsin  26778  atancj  26796  efiatan  26798  atanlogaddlem  26799  cosatan  26807  atantan  26809  atans2  26817  log2cnv  26830  log2tlbnd  26831  birthdaylem2  26838  cxplim  26858  lgamgulmlem2  26916  wilthlem1  26954  basellem3  26969  musum  27077  musumsum  27078  muinv  27079  pclogsum  27102  mersenne  27114  dchrabs  27147  dchrinv  27148  lgseisenlem1  27262  lgsquadlem1  27267  lgsquadlem2  27268  lgsquadlem3  27269  lgsquad2lem1  27271  2lgslem1  27281  2sqmod  27323  chebbnd1lem3  27358  chpchtlim  27366  rplogsumlem2  27372  dchrisumlem2  27377  dchrmusum2  27381  mulog2sumlem1  27421  mulog2sumlem3  27423  vmalogdivsum2  27425  selberg4lem1  27447  pntrlog2bndlem2  27465  pntrlog2bndlem4  27467  pntibndlem2  27478  pntlemr  27489  pntlemf  27492  pntlemo  27494  addsdilem4  28033  mulsunif2lem  28048  halfcut  28309  zs12bday  28319  ragcom  28601  colperpexlem1  28633  lmiisolem  28699  hypcgrlem2  28703  trgcopyeulem  28708  brbtwn2  28808  colinearalglem1  28809  colinearalglem2  28810  axcontlem2  28868  axcontlem8  28874  numedglnl  29047  clwlkclwwlklem2a  29900  numclwlk1lem1  30271  numclwlk1lem2  30272  numclwwlk2  30283  grpoinvid2  30431  ablodivdiv4  30456  smcnlem  30599  ipidsq  30612  ipasslem2  30734  minvecolem2  30777  hv2times  30963  pjhthlem1  31293  pjds3i  31615  ho2times  31721  opsqrlem6  32047  pjclem4  32101  pj3si  32109  csmdsymi  32236  ofoprabco  32561  fcnvgreu  32570  quad3d  32646  swrdrndisj  32852  trsp2cyc  33053  cycpmco2lem3  33058  cycpmco2lem4  33059  cycpmco2lem5  33060  cycpmco2lem6  33061  cycpmco2  33063  conjga  33100  elrgspnlem1  33166  rlocmulval  33193  imaslmod  33297  1arithufdlem3  33490  r1padd1  33546  frlmdim  33580  rrxdim  33583  lbsdiflsp0  33595  fedgmullem1  33598  fedgmullem2  33599  extdg1id  33634  ccfldextdgrr  33640  fldextrspunlem1  33643  constrrtlc1  33695  constrrtcclem  33697  constrrtcc  33698  constrrecl  33732  constrresqrtcl  33740  cos9thpiminplylem1  33745  cos9thpiminplylem2  33746  cos9thpiminplylem3  33747  cos9thpiminply  33751  qqhcn  33954  esumpr2  34030  esumpfinval  34038  esumpfinvalf  34039  carsggect  34282  oddpwdcv  34319  eulerpartlemgs2  34344  fibp1  34365  orvcelval  34433  ballotlemscr  34483  ballotlemfrci  34492  signsplypnf  34514  reprpmtf1o  34590  breprexplemc  34596  breprexp  34597  circlemeth  34604  lpadright  34648  revwlk  35085  subfacp1lem5  35144  cvmliftlem10  35254  circum  35634  faclimlem3  35705  fwddifnp1  36126  bj-bary1lem  37271  tan2h  37579  poimirlem3  37590  poimirlem13  37600  poimirlem14  37601  itgaddnclem1  37645  itgmulc2nclem2  37654  areacirclem1  37675  areacirclem4  37678  istotbnd3  37738  iscringd  37965  3atlem1  39450  pmod2iN  39816  polval2N  39873  lhple  40009  cdleme2  40195  cdleme35d  40419  cdleme42h  40449  cdlemeg46ngfr  40485  cdlemkid1  40889  lcfl7lem  41466  mapdpglem22  41660  mapdh6dN  41706  hdmap1l6d  41780  hdmapinvlem3  41887  lcmineqlem3  41992  nnadddir  42231  readvrec2  42322  readdsub  42345  sn-negex12  42378  zmulcomlem  42428  selvvvval  42546  evlselv  42548  evlsmhpvvval  42556  prjspeclsp  42573  prjspner1  42587  3cubeslem3r  42648  diophin  42733  irrapxlem2  42784  pellexlem6  42795  pell1234qrmulcl  42816  rmxyval  42877  rmxyneg  42882  rmxyadd  42883  jm2.24  42925  jm2.25  42961  limexissupab  43245  omabs2  43294  tfsconcatrev  43310  naddwordnexlem4  43363  snhesn  43748  scottrankd  44210  radcnvrat  44276  binomcxplemnotnn0  44318  sub2times  45244  mul13d  45251  fperiodmullem  45274  fperiodmul  45275  isumneg  45573  climneg  45581  itgsinexp  45926  stoweidlem13  45984  stoweidlem42  46013  wallispilem4  46039  wallispilem5  46040  wallispi2lem1  46042  stirlinglem1  46045  stirlinglem3  46047  stirlinglem4  46048  stirlinglem5  46049  stirlinglem7  46051  stirlinglem10  46054  dirkertrigeqlem3  46071  fourierdlem30  46108  fourierdlem32  46110  fourierdlem42  46120  fourierdlem48  46125  fourierdlem49  46126  fourierdlem83  46160  sqwvfoura  46199  sqwvfourb  46200  etransclem2  46207  etransclem46  46251  sharhght  46836  imasetpreimafvbijlemfv  47376  fmtnorec3  47522  quad1  47594  requad1  47596  ushggricedg  47900  lmodvsmdi  48340  dmatALTbas  48363  ldepsprlem  48434  itcovalt2lem2lem2  48636  ackval3  48645  1subrec1sub  48667  eenglngeehlnmlem1  48699  eenglngeehlnmlem2  48700  itsclc0xyqsolr  48731  swapfid  49241  sinhpcosh  49702