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 set class
Syntax hints:    -> wi 4    = wceq 1653
This theorem is referenced by:  negsub  9351  neg2sub  9363  divmuleq  9721  divneg2  9740  discr  11518  bcpasc  11614  hashgval2  11654  hashf1lem2  11707  crim  11922  remullem  11935  incexclem  12618  isum1p  12623  geo2sum  12652  efi4p  12740  sinhval  12757  addcos  12777  cos2tsin  12782  demoivreALT  12804  rpnnen2lem11  12826  sadaddlem  12980  smumullem  13006  sqgcd  13060  eulerthlem2  13173  omeo  13190  pockthlem  13275  4sqlem10  13317  vdwlem2  13352  vdwlem6  13356  vdwlem8  13358  fuccocl  14163  resssetc  14249  resscatc  14262  uncfcurf  14338  yonedalem3b  14378  prdspjmhm  14768  grpinvid2  14856  imasgrp2  14935  lagsubg2  15003  cntzsubm  15136  sylow3lem2  15264  efgredleme  15377  ablsubsub  15444  ablsubsub4  15445  odadd2  15466  gex2abl  15468  pgpfac1lem3a  15636  abvneg  15924  lsppr  16167  psrass1  16471  resspsradd  16481  resspsrvsca  16483  mplcoe2  16532  mplmon2mul  16563  evlslem2  16570  coe1tm  16667  ply1scl1  16685  gzrngunit  16766  cmpfi  17473  cnconn  17487  txrest  17665  utopsnneiplem  18279  blcvx  18831  tchcphlem2  19195  minveclem2  19329  pjthlem1  19340  uniioovol  19473  uniioombllem2  19477  itg1addlem4  19593  mbfi1fseqlem5  19613  itg2mulc  19641  itg2monolem1  19644  itgaddlem1  19716  itgmulc2lem2  19726  dvrec  19843  lhop2  19901  ftc1lem5  19926  deg1submon1p  20077  plypf1  20133  coefv0  20168  coemulhi  20174  coemulc  20175  dgreq0  20185  dvply1  20203  vieta1  20231  aareccl  20245  aaliou3lem8  20264  dvtaylp  20288  mtest  20322  sineq0  20431  efif1olem2  20447  efif1olem4  20449  tanarg  20516  logtayl2  20555  isosctrlem2  20665  chordthmlem2  20676  chordthmlem4  20678  dcubic1lem  20685  dcubic1  20687  mcubic  20689  dquart  20695  quart1lem  20697  quart1  20698  efiasin  20730  asinsin  20734  atancj  20752  efiatan  20754  atanlogaddlem  20755  cosatan  20763  atantan  20765  atans2  20773  log2cnv  20786  log2tlbnd  20787  birthdaylem2  20793  cxplim  20812  wilthlem1  20853  basellem3  20867  musum  20978  musumsum  20979  muinv  20980  pclogsum  21001  mersenne  21013  dchrabs  21046  dchrinv  21047  lgseisenlem1  21135  lgsquadlem1  21140  lgsquadlem2  21141  lgsquadlem3  21142  lgsquad2lem1  21144  chebbnd1lem3  21167  chpchtlim  21175  rplogsumlem2  21181  dchrisumlem2  21186  dchrmusum2  21190  mulog2sumlem1  21230  mulog2sumlem3  21232  vmalogdivsum2  21234  selberg4lem1  21256  pntrlog2bndlem2  21274  pntrlog2bndlem4  21276  pntibndlem2  21287  pntlemr  21298  pntlemf  21301  pntlemo  21303  grpoinvid2  21821  gxcom  21859  gxmodid  21869  ablodivdiv4  21881  vcoprne  22060  nvnncan  22146  smcnlem  22195  ipidsq  22211  ipasslem2  22335  minvecolem2  22379  hv2times  22565  pjhthlem1  22895  pjds3i  23217  ho2times  23324  opsqrlem6  23650  pjclem4  23704  pj3si  23712  csmdsymi  23839  fmptapd  24063  ofoprabco  24081  qqhcn  24377  nnlogbexp  24406  esumpr2  24460  esumpfinval  24467  esumpfinvalf  24468  orvcelval  24728  ballotlemscr  24778  ballotlemfrci  24787  lgamgulmlem2  24816  subfacp1lem5  24872  cvmliftlem10  24983  fallfacfwd  25354  faclimlem3  25366  brbtwn2  25846  colinearalglem1  25847  colinearalglem2  25848  axcontlem2  25906  axcontlem8  25912  fsumkthpow  26104  bpoly3  26106  bpoly4  26107  mblfinlem2  26246  itgaddnclem1  26265  itgmulc2nclem2  26274  areacirclem1  26294  areacirclem4  26297  istotbnd3  26482  iscringd  26611  diophin  26833  irrapxlem2  26888  pellexlem6  26899  pell1234qrmulcl  26920  rmxyval  26980  rmxyadd  26986  jm2.24  27030  jm2.25  27072  frlmgsum  27211  mamuass  27439  isumneg  27706  climneg  27714  itgsinexp  27727  stoweidlem13  27740  stoweidlem42  27769  wallispilem4  27795  wallispilem5  27796  wallispi2lem1  27798  stirlinglem1  27801  stirlinglem3  27803  stirlinglem4  27804  stirlinglem5  27805  stirlinglem7  27807  stirlinglem10  27810  sharhght  27833  sinhpcosh  28545  3atlem1  30342  pmod2iN  30708  polval2N  30765  lhple  30901  cdleme2  31087  cdleme35d  31311  cdleme42h  31341  cdlemeg46ngfr  31377  cdlemkid1  31781  lcfl7lem  32359  mapdpglem22  32553  mapdh6dN  32599  hdmap1l6d  32674  hdmapinvlem3  32783
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431
  Copyright terms: Public domain W3C validator