Theorem 3eqtr2d 2774

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 2771	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtrd 2768	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 2123  ax-ext 2705

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

This theorem is referenced by:  fmptapd  7114  negsub  11420  neg2sub  11432  divmuleq  11837  divneg2  11856  discr  14154  bcpasc  14235  hashgval2  14292  hashf1lem2  14370  relexpaddnn  14965  crim  15029  remullem  15042  isum1p  15755  geo2sum  15787  fallfacfwd  15950  fsumkthpow  15970  bpoly3  15972  bpoly4  15973  efi4p  16053  sinhval  16070  addcos  16090  cos2tsin  16095  demoivreALT  16117  rpnnen2lem11  16140  omeo  16284  pwp1fsum  16309  sadaddlem  16384  bitsres  16391  smumullem  16410  sqgcd  16480  expgcd  16481  eulerthlem2  16700  vfermltlALT  16721  pockthlem  16824  4sqlem10  16866  vdwlem2  16901  vdwlem6  16905  vdwlem8  16907  fuccocl  17882  resssetc  18007  resscatc  18024  uncfcurf  18153  yonedalem3b  18193  prdspjmhm  18745  grpinvid2  18913  imasgrp2  18976  mulgaddcomlem  19018  mulgmodid  19034  lagsubg2  19114  cntzsgrpcl  19254  cntzsubm  19258  sylow3lem2  19548  efgredleme  19663  ablsubsub  19737  ablsubsub4  19738  odadd2  19769  gex2abl  19771  pgpfac1lem3a  19998  pwspjmhmmgpd  20254  rngcid  20559  ringcid  20588  abvneg  20750  lmodfopne  20842  lsppr  21036  rngqiprngfulem4  21260  gzrngunit  21379  frlmsubgval  21711  frlmgsum  21718  psrass1  21910  resspsradd  21921  resspsrvsca  21923  mplcoe5  21986  mplmon2mul  22015  evlslem2  22025  evlsvarsrng  22053  coe1tm  22206  ply1scl1OLD  22227  ply1fermltlchr  22247  evls1varsrng  22275  mamuass  22337  mavmulass  22484  mulmarep1gsum2  22509  mdetuni0  22556  maducoeval2  22575  madulid  22580  mat2pmatmul  22666  decpmatmulsumfsupp  22708  pmatcollpwlem  22715  pm2mpmhmlem1  22753  cmpfi  23343  cnconn  23357  txrest  23566  utopsnneiplem  24182  blcvx  24733  tcphcphlem2  25183  cphipval2  25188  cphipval  25190  rrx0  25344  minveclem2  25373  pjthlem1  25384  uniioovol  25527  uniioombllem2  25531  itg1addlem4  25647  mbfi1fseqlem5  25667  itg2mulc  25695  itg2monolem1  25698  itgaddlem1  25771  itgmulc2lem2  25781  dvrec  25906  lhop2  25967  ftc1lem5  25994  deg1submon1p  26105  plypf1  26164  coefv0  26200  coemulhi  26206  coemulc  26207  dgreq0  26218  dvply1  26238  vieta1  26267  aareccl  26281  aaliou3lem8  26300  dvtaylp  26325  mtest  26360  sineq0  26480  efif1olem2  26499  efif1olem4  26501  tanarg  26575  logtayl2  26618  nnlogbexp  26738  isosctrlem2  26776  chordthmlem2  26790  chordthmlem4  26792  heron  26795  dcubic1lem  26800  dcubic1  26802  mcubic  26804  dquart  26810  quart1lem  26812  quart1  26813  efiasin  26845  asinsin  26849  atancj  26867  efiatan  26869  atanlogaddlem  26870  cosatan  26878  atantan  26880  atans2  26888  log2cnv  26901  log2tlbnd  26902  birthdaylem2  26909  cxplim  26929  lgamgulmlem2  26987  wilthlem1  27025  basellem3  27040  musum  27148  musumsum  27149  muinv  27150  pclogsum  27173  mersenne  27185  dchrabs  27218  dchrinv  27219  lgseisenlem1  27333  lgsquadlem1  27338  lgsquadlem2  27339  lgsquadlem3  27340  lgsquad2lem1  27342  2lgslem1  27352  2sqmod  27394  chebbnd1lem3  27429  chpchtlim  27437  rplogsumlem2  27443  dchrisumlem2  27448  dchrmusum2  27452  mulog2sumlem1  27492  mulog2sumlem3  27494  vmalogdivsum2  27496  selberg4lem1  27518  pntrlog2bndlem2  27536  pntrlog2bndlem4  27538  pntibndlem2  27549  pntlemr  27560  pntlemf  27563  pntlemo  27565  addsdilem4  28113  mulsunif2lem  28128  halfcut  28398  zs12bday  28414  ragcom  28696  colperpexlem1  28728  lmiisolem  28794  hypcgrlem2  28798  trgcopyeulem  28803  brbtwn2  28904  colinearalglem1  28905  colinearalglem2  28906  axcontlem2  28964  axcontlem8  28970  numedglnl  29143  clwlkclwwlklem2a  29999  numclwlk1lem1  30370  numclwlk1lem2  30371  numclwwlk2  30382  grpoinvid2  30530  ablodivdiv4  30555  smcnlem  30698  ipidsq  30711  ipasslem2  30833  minvecolem2  30876  hv2times  31062  pjhthlem1  31392  pjds3i  31714  ho2times  31820  opsqrlem6  32146  pjclem4  32200  pj3si  32208  csmdsymi  32335  ofoprabco  32668  fcnvgreu  32677  quad3d  32757  nn0diffz0  32802  swrdrndisj  32967  trsp2cyc  33133  cycpmco2lem3  33138  cycpmco2lem4  33139  cycpmco2lem5  33140  cycpmco2lem6  33141  cycpmco2  33143  conjga  33180  elrgspnlem1  33252  rlocmulval  33279  imaslmod  33362  1arithufdlem3  33555  deg1prod  33592  r1padd1  33617  mplvrpmrhm  33640  frlmdim  33696  rrxdim  33699  lbsdiflsp0  33711  fedgmullem1  33714  fedgmullem2  33715  extdg1id  33751  ccfldextdgrr  33757  fldextrspunlem1  33760  constrrtlc1  33817  constrrtcclem  33819  constrrtcc  33820  constrrecl  33854  constrresqrtcl  33862  cos9thpiminplylem1  33867  cos9thpiminplylem2  33868  cos9thpiminplylem3  33869  cos9thpiminply  33873  qqhcn  34076  esumpr2  34152  esumpfinval  34160  esumpfinvalf  34161  carsggect  34403  oddpwdcv  34440  eulerpartlemgs2  34465  fibp1  34486  orvcelval  34554  ballotlemscr  34604  ballotlemfrci  34613  signsplypnf  34635  reprpmtf1o  34711  breprexplemc  34717  breprexp  34718  circlemeth  34725  lpadright  34769  revwlk  35241  subfacp1lem5  35300  cvmliftlem10  35410  circum  35790  faclimlem3  35861  fwddifnp1  36281  bj-bary1lem  37427  tan2h  37725  poimirlem3  37736  poimirlem13  37746  poimirlem14  37747  itgaddnclem1  37791  itgmulc2nclem2  37800  areacirclem1  37821  areacirclem4  37824  istotbnd3  37884  iscringd  38111  3atlem1  39655  pmod2iN  40021  polval2N  40078  lhple  40214  cdleme2  40400  cdleme35d  40624  cdleme42h  40654  cdlemeg46ngfr  40690  cdlemkid1  41094  lcfl7lem  41671  mapdpglem22  41865  mapdh6dN  41911  hdmap1l6d  41985  hdmapinvlem3  42092  lcmineqlem3  42197  nnadddir  42440  readvrec2  42531  readdsub  42554  sn-negex12  42587  zmulcomlem  42637  selvvvval  42743  evlselv  42745  evlsmhpvvval  42753  prjspeclsp  42770  prjspner1  42784  3cubeslem3r  42844  diophin  42929  irrapxlem2  42980  pellexlem6  42991  pell1234qrmulcl  43012  rmxyval  43072  rmxyneg  43077  rmxyadd  43078  jm2.24  43120  jm2.25  43156  limexissupab  43440  omabs2  43489  tfsconcatrev  43505  naddwordnexlem4  43558  snhesn  43943  scottrankd  44405  radcnvrat  44471  binomcxplemnotnn0  44513  sub2times  45437  mul13d  45444  fperiodmullem  45467  fperiodmul  45468  isumneg  45764  climneg  45772  itgsinexp  46115  stoweidlem13  46173  stoweidlem42  46202  wallispilem4  46228  wallispilem5  46229  wallispi2lem1  46231  stirlinglem1  46234  stirlinglem3  46236  stirlinglem4  46237  stirlinglem5  46238  stirlinglem7  46240  stirlinglem10  46243  dirkertrigeqlem3  46260  fourierdlem30  46297  fourierdlem32  46299  fourierdlem42  46309  fourierdlem48  46314  fourierdlem49  46315  fourierdlem83  46349  sqwvfoura  46388  sqwvfourb  46389  etransclem2  46396  etransclem46  46440  sharhght  47025  imasetpreimafvbijlemfv  47564  fmtnorec3  47710  quad1  47782  requad1  47784  ushggricedg  48089  lmodvsmdi  48541  dmatALTbas  48563  ldepsprlem  48634  itcovalt2lem2lem2  48836  ackval3  48845  1subrec1sub  48867  eenglngeehlnmlem1  48899  eenglngeehlnmlem2  48900  itsclc0xyqsolr  48931  swapfid  49440  sinhpcosh  49901