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

Theorem simpr2 995
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpr2  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ch )

Proof of Theorem simpr2
StepHypRef Expression
1 simp2 989 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
21adantl 466 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  simplr2  1031  simprr2  1037  simp1r2  1085  simp2r2  1091  simp3r2  1097  3anandis  1320  wereu  4721  isopolem  6041  fr3nr  6396  frfi  7562  intrnfi  7671  fisupcl  7722  cnfcomlem  7937  cnfcomlemOLD  7945  ackbij1lem15  8408  cofsmo  8443  sornom  8451  fpwwe2lem5  8806  dedekindle  9539  supmul1  10300  uzletr  10874  xlesubadd  11231  elioc2  11363  elico2  11364  elicc2  11365  fz0fzelfz0  11491  fseq1p1m1  11539  swrdsymbeq  12346  ccatswrd  12355  swrdswrdlem  12358  tanadd  13456  dvds2ln  13568  cshwsidrepsw  14125  ressress  14240  f1ovscpbl  14469  mreexexlem4d  14590  mreexexd  14591  iscatd2  14624  2oppccomf  14669  issubc3  14764  fthmon  14842  fuccocl  14879  fucidcl  14880  invfuc  14889  curf2cl  15046  yonedalem4c  15092  yonedalem3  15095  pospo  15148  latjle12  15237  latjlej1  15240  latnlej2  15246  latlem12  15253  latmlem1  15256  latledi  15264  latjass  15270  latj12  15271  latj32  15272  latj13  15273  latj31  15274  latjrot  15275  latjjdi  15278  latjjdir  15279  latdisdlem  15364  prdsmndd  15459  frmdmnd  15542  grpsubrcan  15612  grpsubadd  15618  grpaddsubass  15620  grpsubsub4  15623  grppnpcan2  15624  grpnpncan  15625  mulgnndir  15654  mulgnn0dir  15655  mulgdir  15657  mulgnnass  15660  mulgnn0ass  15661  mulgass  15662  mulgsubdir  15663  pwsmulg  15674  issubg2  15701  eqgval  15735  divsgrp  15741  galcan  15827  gacan  15828  oppgmnd  15874  symggrp  15910  fvcosymgeq  15939  pmtrprfv  15964  psgnunilem3  16007  cmn32  16300  cmn12  16302  abladdsub  16309  mulgdi  16319  mulgsubdi  16322  dprdss  16531  dprdz  16532  dprdf1o  16534  dprdsn  16538  dprd2da  16546  dmdprdsplit  16551  ablfac1b  16576  pgpfac1lem5  16585  srgi  16618  srgbinom  16648  rngi  16662  prdsrngd  16709  opprrng  16728  mulgass3  16734  dvrass  16787  subrgunit  16888  issubrg2  16890  abvdiv  16927  lsssn0  17034  islss3  17045  prdslmodd  17055  islmhm2  17124  lspsolv  17229  islbs2  17240  islbs3  17241  lbsextlem4  17247  sralmod  17273  issubassa  17400  sraassa  17401  psrbaglesupp  17440  psrbaglesuppOLD  17441  psrbaglecl  17442  psrbagcon  17445  psrgrp  17474  psrlmod  17477  psrrng  17488  psrassa  17491  psgndiflemB  18035  ipdir  18073  ipdi  18074  ipsubdir  18076  ipsubdi  18077  ipass  18079  ipassr  18080  ipassr2  18081  isphld  18088  ocvlss  18102  mamudm  18293  matrng  18335  matassa  18336  ofco2  18337  ma1repveval  18387  mdetunilem1  18423  mdetunilem9  18431  iinopn  18520  restopnb  18784  subbascn  18863  nrmsep2  18965  isnrm3  18968  regsep2  18985  dnsconst  18987  dfcon2  19028  1stcelcls  19070  dislly  19106  ptuni2  19154  tx1stc  19228  0nelfb  19409  infil  19441  fsubbas  19445  filssufilg  19489  hauspwpwf1  19565  cnextcn  19644  tmdcn2  19665  ustuqtoplem  19819  utopsnneiplem  19827  psmettri  19892  isxmet2d  19907  xmettri  19931  xmetres2  19941  bldisj  19978  blss2ps  19983  blss2  19984  xmstri2  20046  mstri2  20047  xmstri  20048  mstri  20049  xmstri3  20050  mstri3  20051  msrtri  20052  comet  20093  stdbdbl  20097  met2ndci  20102  ngprcan  20206  ngplcan  20207  ngpsubcan  20210  nrgdsdi  20251  nrgdsdir  20252  nlmdsdi  20267  nlmdsdir  20268  blcvx  20380  icoopnst  20516  pi1grplem  20626  cvsdiv  20686  cvsdivcl  20687  cphdivcl  20706  cphsubdir  20731  cphsubdi  20732  tchcph  20757  bcthlem5  20844  volfiniun  21033  volcn  21091  itg1val2  21167  dvconst  21396  dvlip  21470  ftc1a  21514  ulmval  21850  ulmdvlem3  21872  ang180  22215  cvxcl  22383  scvxcvx  22384  sgmmul  22545  dchrabl  22598  f1otrge  23123  xmstrkgc  23137  colinearalglem1  23157  axcgrtr  23166  axeuclidlem  23213  axcontlem3  23217  axcontlem4  23218  axcontlem7  23221  eengtrkg  23236  eengtrkge  23237  isspthonpth  23488  wlkdvspth  23512  iseupa  23591  grpomuldivass  23741  grponpncan  23747  grpodiveq  23748  ablomuldiv  23781  ablodivdiv4  23783  ablonnncan1  23787  nvmdi  24035  nvsubadd  24040  dipassr  24251  archiabllem2c  26217  dvrdir  26263  dvrcan5  26266  reofld  26313  pstmfval  26328  qqhval2lem  26415  qqhvq  26421  measdivcstOLD  26643  measdivcst  26644  erdszelem9  27092  rescon  27140  cvmseu  27170  cvmlift2lem10  27206  cvmlift2lem12  27208  frrlem4  27776  cgrid2  28039  segconeu  28047  btwncomim  28049  btwnswapid  28053  trisegint  28064  cgrxfr  28091  brofs2  28113  endofsegid  28121  btwnconn2  28138  seglemin  28149  segletr  28150  btwnsegle  28153  colinbtwnle  28154  broutsideof2  28158  btwnoutside  28161  broutsideof3  28162  outsideoftr  28165  outsidele  28168  fvray  28177  fvline  28180  ellines  28188  ftc1anc  28480  sdclem1  28644  sstotbnd2  28678  iscringd  28804  irrapxlem6  29173  jm2.26lem3  29355  dgrsub2  29496  mpaaroot  29517  mendrng  29554  mendlmod  29555  mendassa  29556  rfcnpre3  29760  fmuldfeq  29769  stoweidlem43  29843  stoweidlem52  29852  stoweidlem53  29853  stoweidlem56  29856  stoweidlem57  29857  stoweidlem60  29860  uzuzle  30195  el2spthonot0  30395  usg2wotspth  30408  2spontn0vne  30411  ltsubsubaddltsub  30472  clwlkfoclwwlk  30523  rusgranumwlks  30579  rusgranumwwlkg  30582  3vfriswmgra  30602  frgrareggt1  30714  ldepsprlem  31011  lincresunit3  31020  lincreslvec3  31021  bnj1098  31782  bnj149  31873  bnj1118  31980  lsmsat  32658  lfladdcl  32721  lflnegcl  32725  lflvscl  32727  eqlkr  32749  lshpkrlem4  32763  lshpkrlem6  32765  ldualgrplem  32795  lduallmodlem  32802  latmassOLD  32879  latm12  32880  latm32  32881  latmrot  32882  latmmdiN  32884  latmmdir  32885  omlfh1N  32908  omlfh3N  32909  cvrnbtwn2  32925  cvlexchb1  32980  cvlsupr2  32993  hlatjass  33019  hlatj12  33020  hlatj32  33021  cvrat  33071  cvrat2  33078  atltcvr  33084  atexchltN  33090  cvrat3  33091  cvrat4  33092  atbtwnexOLDN  33096  atbtwnex  33097  3dimlem3  33110  3dimlem3OLDN  33111  3at  33139  2atneat  33164  llncmp  33171  2at0mat0  33174  2atmat0  33175  llncvrlpln  33207  lplncmp  33211  2llnjaN  33215  4atlem11  33258  lplncvrlvol  33265  lvolcmp  33266  2atm2atN  33434  elpaddatriN  33452  paddasslem8  33476  paddass  33487  padd12N  33488  paddssw2  33493  paddss  33494  pmod1i  33497  pmodN  33499  pmapjlln1  33504  atmod1i1  33506  atmod1i2  33508  pexmidlem2N  33620  pl42lem2N  33629  pl42lem3N  33630  pl42lem4N  33631  pl42N  33632  lhpm0atN  33678  lautlt  33740  lautcvr  33741  lautj  33742  lautm  33743  ltrneq2  33797  cdlemd1  33847  cdleme1b  33875  cdleme1  33876  cdleme2  33877  cdleme3e  33881  cdlemefr27cl  34052  cdlemefs27cl  34062  cdleme42ke  34134  cdleme42mN  34136  cdlemf2  34211  cdlemftr2  34215  trljco  34389  tgrpgrplem  34398  tendoplass  34432  tendodi1  34433  tendodi2  34434  cdlemk34  34559  cdlemk36  34562  erngdvlem3-rN  34647  tendospdi1  34670  dialss  34696  dvhvaddass  34747  dvhopvsca  34752  dvhlveclem  34758  diblss  34820  diclss  34843  diclspsn  34844  cdlemn11pre  34860  dihmeetlem12N  34968  dihmeetlem16N  34972  dihmeetlem17N  34973  dihmeetlem18N  34974  dvh4dimN  35097  lpolconN  35137  dochpolN  35140  lclkr  35183  lclkrs  35189  lcfr  35235
  Copyright terms: Public domain W3C validator