MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr2d Structured version   Unicode version

Theorem 3eqtr2d 2476
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3eqtr2d.1  |-  ( ph  ->  A  =  B )
3eqtr2d.2  |-  ( ph  ->  C  =  B )
3eqtr2d.3  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
3eqtr2d  |-  ( ph  ->  A  =  D )

Proof of Theorem 3eqtr2d
StepHypRef Expression
1 3eqtr2d.1 . . 3  |-  ( ph  ->  A  =  B )
2 3eqtr2d.2 . . 3  |-  ( ph  ->  C  =  B )
31, 2eqtr4d 2473 . 2  |-  ( ph  ->  A  =  C )
4 3eqtr2d.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtrd 2470 1  |-  ( ph  ->  A  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-cleq 2421
This theorem is referenced by:  fmptapd  6103  negsub  9921  neg2sub  9933  divmuleq  10311  divneg2  10330  discr  12406  bcpasc  12503  hashgval2  12554  hashf1lem2  12614  relexpaddnn  13093  crim  13157  remullem  13170  incexclem  13872  isum1p  13877  geo2sum  13907  fallfacfwd  14067  fsumkthpow  14087  bpoly3  14089  bpoly4  14090  efi4p  14169  sinhval  14186  addcos  14206  cos2tsin  14211  demoivreALT  14233  rpnnen2lem11  14255  sadaddlem  14414  smumullem  14440  sqgcd  14497  eulerthlem2  14699  vfermltlALT  14716  omeo  14727  pockthlem  14812  4sqlem10  14854  vdwlem2  14895  vdwlem6  14899  vdwlem8  14901  fuccocl  15820  resssetc  15938  resscatc  15951  uncfcurf  16075  yonedalem3b  16115  prdspjmhm  16565  grpinvid2  16666  imasgrp2  16752  lagsubg2  16829  cntzsubm  16940  sylow3lem2  17215  efgredleme  17328  ablsubsub  17395  ablsubsub4  17396  odadd2  17422  gex2abl  17424  pgpfac1lem3a  17644  abvneg  17997  lsppr  18251  psrass1  18564  resspsradd  18575  resspsrvsca  18577  mplcoe5  18627  mplmon2mul  18659  evlslem2  18670  evlsvarsrng  18686  coe1tm  18801  ply1scl1  18820  evls1varsrng  18863  gzrngunit  18968  frlmsubgval  19258  frlmgsum  19261  mamuass  19358  mavmulass  19505  mulmarep1gsum2  19530  mdetuni0  19577  maducoeval2  19596  madulid  19601  mat2pmatmul  19686  decpmatmulsumfsupp  19728  pmatcollpwlem  19735  pm2mpmhmlem1  19773  cmpfi  20354  cnconn  20368  txrest  20577  utopsnneiplem  21193  blcvx  21727  tchcphlem2  22103  minveclem2  22261  pjthlem1  22272  uniioovol  22413  uniioombllem2  22417  uniioombllem2OLD  22418  itg1addlem4  22534  mbfi1fseqlem5  22554  itg2mulc  22582  itg2monolem1  22585  itgaddlem1  22657  itgmulc2lem2  22667  dvrec  22786  lhop2  22844  ftc1lem5  22869  deg1submon1p  22978  plypf1  23034  coefv0  23070  coemulhi  23076  coemulc  23077  dgreq0  23087  dvply1  23105  vieta1  23133  aareccl  23147  aaliou3lem8  23166  dvtaylp  23190  mtest  23224  sineq0  23341  efif1olem2  23357  efif1olem4  23359  tanarg  23433  logtayl2  23472  nnlogbexp  23583  isosctrlem2  23613  chordthmlem2  23624  chordthmlem4  23626  heron  23629  dcubic1lem  23634  dcubic1  23636  mcubic  23638  dquart  23644  quart1lem  23646  quart1  23647  efiasin  23679  asinsin  23683  atancj  23701  efiatan  23703  atanlogaddlem  23704  cosatan  23712  atantan  23714  atans2  23722  log2cnv  23735  log2tlbnd  23736  birthdaylem2  23743  cxplim  23762  lgamgulmlem2  23820  wilthlem1  23858  basellem3  23872  musum  23983  musumsum  23984  muinv  23985  pclogsum  24006  mersenne  24018  dchrabs  24051  dchrinv  24052  lgseisenlem1  24140  lgsquadlem1  24145  lgsquadlem2  24146  lgsquadlem3  24147  lgsquad2lem1  24149  chebbnd1lem3  24172  chpchtlim  24180  rplogsumlem2  24186  dchrisumlem2  24191  dchrmusum2  24195  mulog2sumlem1  24235  mulog2sumlem3  24237  vmalogdivsum2  24239  selberg4lem1  24261  pntrlog2bndlem2  24279  pntrlog2bndlem4  24281  pntibndlem2  24292  pntlemr  24303  pntlemf  24306  pntlemo  24308  ragcom  24600  colperpexlem1  24629  lmiisolem  24694  hypcgrlem2  24698  trgcopyeulem  24703  brbtwn2  24781  colinearalglem1  24782  colinearalglem2  24783  axcontlem2  24841  axcontlem8  24847  clwlkisclwwlklem2a  25358  numclwwlk2  25680  grpoinvid2  25804  gxcom  25842  gxmodid  25852  ablodivdiv4  25864  vcoprne  26043  nvnncan  26129  smcnlem  26178  ipidsq  26194  ipasslem2  26318  minvecolem2  26362  hv2times  26549  pjhthlem1  26879  pjds3i  27201  ho2times  27307  opsqrlem6  27633  pjclem4  27687  pj3si  27695  csmdsymi  27822  ofoprabco  28107  fcnvgreu  28115  2sqmod  28247  qqhcn  28634  esumpr2  28727  esumpfinval  28735  esumpfinvalf  28736  carsggect  28979  oddpwdcv  29014  eulerpartlemgs2  29039  fibp1  29060  orvcelval  29127  ballotlemscr  29177  ballotlemfrci  29186  signsplypnf  29227  subfacp1lem5  29695  cvmliftlem10  29805  circum  30106  faclimlem3  30168  fwddifnp1  30717  bj-bary1lem  31460  tan2h  31640  poimirlem3  31646  poimirlem13  31656  poimirlem14  31657  mblfinlem2  31681  itgaddnclem1  31703  itgmulc2nclem2  31712  areacirclem1  31735  areacirclem4  31738  istotbnd3  31806  iscringd  31935  3atlem1  32756  pmod2iN  33122  polval2N  33179  lhple  33315  cdleme2  33502  cdleme35d  33727  cdleme42h  33757  cdlemeg46ngfr  33793  cdlemkid1  34197  lcfl7lem  34775  mapdpglem22  34969  mapdh6dN  35015  hdmap1l6d  35090  hdmapinvlem3  35199  diophin  35323  irrapxlem2  35376  pellexlem6  35387  pell1234qrmulcl  35408  rmxyval  35468  rmxyneg  35473  rmxyadd  35474  jm2.24  35518  jm2.25  35559  snhesn  36018  radcnvrat  36299  binomcxplemnotnn0  36341  sub2times  37091  mul13d  37097  fperiodmullem  37129  fperiodmul  37130  isumneg  37251  climneg  37260  itgsinexp  37399  stoweidlem13  37441  stoweidlem42  37471  wallispilem4  37498  wallispilem5  37499  wallispi2lem1  37501  stirlinglem1  37504  stirlinglem3  37506  stirlinglem4  37507  stirlinglem5  37508  stirlinglem7  37510  stirlinglem10  37513  dirkertrigeqlem3  37530  fourierdlem30  37567  fourierdlem32  37569  fourierdlem42  37579  fourierdlem48  37585  fourierdlem49  37586  fourierdlem83  37620  sqwvfoura  37659  sqwvfourb  37660  etransclem2  37667  etransclem46  37711  sharhght  37873  rngcid  38738  ringcid  38784  lmodvsmdi  38926  dmatALTbas  38953  ldepsprlem  39024  sinhpcosh  39220
  Copyright terms: Public domain W3C validator