Theorem 3eqtr2d 2771

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2722

This theorem is referenced by:  fmptapd  7100  negsub  11401  neg2sub  11413  divmuleq  11818  divneg2  11837  discr  14139  bcpasc  14220  hashgval2  14277  hashf1lem2  14355  relexpaddnn  14950  crim  15014  remullem  15027  isum1p  15740  geo2sum  15772  fallfacfwd  15935  fsumkthpow  15955  bpoly3  15957  bpoly4  15958  efi4p  16038  sinhval  16055  addcos  16075  cos2tsin  16080  demoivreALT  16102  rpnnen2lem11  16125  omeo  16269  pwp1fsum  16294  sadaddlem  16369  bitsres  16376  smumullem  16395  sqgcd  16465  expgcd  16466  eulerthlem2  16685  vfermltlALT  16706  pockthlem  16809  4sqlem10  16851  vdwlem2  16886  vdwlem6  16890  vdwlem8  16892  fuccocl  17866  resssetc  17991  resscatc  18008  uncfcurf  18137  yonedalem3b  18177  prdspjmhm  18729  grpinvid2  18897  imasgrp2  18960  mulgaddcomlem  19002  mulgmodid  19018  lagsubg2  19099  cntzsgrpcl  19239  cntzsubm  19243  sylow3lem2  19533  efgredleme  19648  ablsubsub  19722  ablsubsub4  19723  odadd2  19754  gex2abl  19756  pgpfac1lem3a  19983  pwspjmhmmgpd  20239  rngcid  20543  ringcid  20572  abvneg  20734  lmodfopne  20826  lsppr  21020  rngqiprngfulem4  21244  gzrngunit  21363  frlmsubgval  21695  frlmgsum  21702  psrass1  21894  resspsradd  21905  resspsrvsca  21907  mplcoe5  21968  mplmon2mul  21997  evlslem2  22007  evlsvarsrng  22027  coe1tm  22180  ply1scl1OLD  22201  ply1fermltlchr  22220  evls1varsrng  22248  mamuass  22310  mavmulass  22457  mulmarep1gsum2  22482  mdetuni0  22529  maducoeval2  22548  madulid  22553  mat2pmatmul  22639  decpmatmulsumfsupp  22681  pmatcollpwlem  22688  pm2mpmhmlem1  22726  cmpfi  23316  cnconn  23330  txrest  23539  utopsnneiplem  24155  blcvx  24706  tcphcphlem2  25156  cphipval2  25161  cphipval  25163  rrx0  25317  minveclem2  25346  pjthlem1  25357  uniioovol  25500  uniioombllem2  25504  itg1addlem4  25620  mbfi1fseqlem5  25640  itg2mulc  25668  itg2monolem1  25671  itgaddlem1  25744  itgmulc2lem2  25754  dvrec  25879  lhop2  25940  ftc1lem5  25967  deg1submon1p  26078  plypf1  26137  coefv0  26173  coemulhi  26179  coemulc  26180  dgreq0  26191  dvply1  26211  vieta1  26240  aareccl  26254  aaliou3lem8  26273  dvtaylp  26298  mtest  26333  sineq0  26453  efif1olem2  26472  efif1olem4  26474  tanarg  26548  logtayl2  26591  nnlogbexp  26711  isosctrlem2  26749  chordthmlem2  26763  chordthmlem4  26765  heron  26768  dcubic1lem  26773  dcubic1  26775  mcubic  26777  dquart  26783  quart1lem  26785  quart1  26786  efiasin  26818  asinsin  26822  atancj  26840  efiatan  26842  atanlogaddlem  26843  cosatan  26851  atantan  26853  atans2  26861  log2cnv  26874  log2tlbnd  26875  birthdaylem2  26882  cxplim  26902  lgamgulmlem2  26960  wilthlem1  26998  basellem3  27013  musum  27121  musumsum  27122  muinv  27123  pclogsum  27146  mersenne  27158  dchrabs  27191  dchrinv  27192  lgseisenlem1  27306  lgsquadlem1  27311  lgsquadlem2  27312  lgsquadlem3  27313  lgsquad2lem1  27315  2lgslem1  27325  2sqmod  27367  chebbnd1lem3  27402  chpchtlim  27410  rplogsumlem2  27416  dchrisumlem2  27421  dchrmusum2  27425  mulog2sumlem1  27465  mulog2sumlem3  27467  vmalogdivsum2  27469  selberg4lem1  27491  pntrlog2bndlem2  27509  pntrlog2bndlem4  27511  pntibndlem2  27522  pntlemr  27533  pntlemf  27536  pntlemo  27538  addsdilem4  28086  mulsunif2lem  28101  halfcut  28371  zs12bday  28387  ragcom  28669  colperpexlem1  28701  lmiisolem  28767  hypcgrlem2  28771  trgcopyeulem  28776  brbtwn2  28876  colinearalglem1  28877  colinearalglem2  28878  axcontlem2  28936  axcontlem8  28942  numedglnl  29115  clwlkclwwlklem2a  29968  numclwlk1lem1  30339  numclwlk1lem2  30340  numclwwlk2  30351  grpoinvid2  30499  ablodivdiv4  30524  smcnlem  30667  ipidsq  30680  ipasslem2  30802  minvecolem2  30845  hv2times  31031  pjhthlem1  31361  pjds3i  31683  ho2times  31789  opsqrlem6  32115  pjclem4  32169  pj3si  32177  csmdsymi  32304  ofoprabco  32636  fcnvgreu  32645  quad3d  32723  swrdrndisj  32928  trsp2cyc  33082  cycpmco2lem3  33087  cycpmco2lem4  33088  cycpmco2lem5  33089  cycpmco2lem6  33090  cycpmco2  33092  conjga  33129  elrgspnlem1  33199  rlocmulval  33226  imaslmod  33308  1arithufdlem3  33501  r1padd1  33558  mplvrpmrhm  33567  frlmdim  33614  rrxdim  33617  lbsdiflsp0  33629  fedgmullem1  33632  fedgmullem2  33633  extdg1id  33669  ccfldextdgrr  33675  fldextrspunlem1  33678  constrrtlc1  33735  constrrtcclem  33737  constrrtcc  33738  constrrecl  33772  constrresqrtcl  33780  cos9thpiminplylem1  33785  cos9thpiminplylem2  33786  cos9thpiminplylem3  33787  cos9thpiminply  33791  qqhcn  33994  esumpr2  34070  esumpfinval  34078  esumpfinvalf  34079  carsggect  34321  oddpwdcv  34358  eulerpartlemgs2  34383  fibp1  34404  orvcelval  34472  ballotlemscr  34522  ballotlemfrci  34531  signsplypnf  34553  reprpmtf1o  34629  breprexplemc  34635  breprexp  34636  circlemeth  34643  lpadright  34687  revwlk  35137  subfacp1lem5  35196  cvmliftlem10  35306  circum  35686  faclimlem3  35757  fwddifnp1  36178  bj-bary1lem  37323  tan2h  37631  poimirlem3  37642  poimirlem13  37652  poimirlem14  37653  itgaddnclem1  37697  itgmulc2nclem2  37706  areacirclem1  37727  areacirclem4  37730  istotbnd3  37790  iscringd  38017  3atlem1  39501  pmod2iN  39867  polval2N  39924  lhple  40060  cdleme2  40246  cdleme35d  40470  cdleme42h  40500  cdlemeg46ngfr  40536  cdlemkid1  40940  lcfl7lem  41517  mapdpglem22  41711  mapdh6dN  41757  hdmap1l6d  41831  hdmapinvlem3  41938  lcmineqlem3  42043  nnadddir  42282  readvrec2  42373  readdsub  42396  sn-negex12  42429  zmulcomlem  42479  selvvvval  42597  evlselv  42599  evlsmhpvvval  42607  prjspeclsp  42624  prjspner1  42638  3cubeslem3r  42699  diophin  42784  irrapxlem2  42835  pellexlem6  42846  pell1234qrmulcl  42867  rmxyval  42927  rmxyneg  42932  rmxyadd  42933  jm2.24  42975  jm2.25  43011  limexissupab  43295  omabs2  43344  tfsconcatrev  43360  naddwordnexlem4  43413  snhesn  43798  scottrankd  44260  radcnvrat  44326  binomcxplemnotnn0  44368  sub2times  45293  mul13d  45300  fperiodmullem  45323  fperiodmul  45324  isumneg  45621  climneg  45629  itgsinexp  45972  stoweidlem13  46030  stoweidlem42  46059  wallispilem4  46085  wallispilem5  46086  wallispi2lem1  46088  stirlinglem1  46091  stirlinglem3  46093  stirlinglem4  46094  stirlinglem5  46095  stirlinglem7  46097  stirlinglem10  46100  dirkertrigeqlem3  46117  fourierdlem30  46154  fourierdlem32  46156  fourierdlem42  46166  fourierdlem48  46171  fourierdlem49  46172  fourierdlem83  46206  sqwvfoura  46245  sqwvfourb  46246  etransclem2  46253  etransclem46  46297  sharhght  46882  imasetpreimafvbijlemfv  47412  fmtnorec3  47558  quad1  47630  requad1  47632  ushggricedg  47937  lmodvsmdi  48389  dmatALTbas  48412  ldepsprlem  48483  itcovalt2lem2lem2  48685  ackval3  48694  1subrec1sub  48716  eenglngeehlnmlem1  48748  eenglngeehlnmlem2  48749  itsclc0xyqsolr  48780  swapfid  49290  sinhpcosh  49751