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

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

Proof of Theorem simpr1
StepHypRef Expression
1 simp1 988 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
21adantl 466 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ps )
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:  simplr1  1030  simprr1  1036  simp1r1  1084  simp2r1  1090  simp3r1  1096  3anandis  1320  isopolem  6031  fr3nr  6386  suppfnss  6709  frfi  7549  intrnfi  7658  iinfi  7659  eqsup  7698  fisupcl  7709  cnfcomlem  7924  cnfcomlemOLD  7932  ackbij1lem15  8395  fpwwe2lem5  8793  dedekindle  9526  ico0  11338  elioc2  11350  elico2  11351  elicc2  11352  iccsplit  11410  elfzelfzelfz  11476  fseq1p1m1  11526  hashtpg  12178  swrdsymbeq  12333  ccatswrd  12342  tanadd  13443  dvds2ln  13555  qredeq  13784  ressress  14227  mreexexlem4d  14577  mreexexd  14578  0catg  14617  2oppccomf  14656  issubc3  14751  fthmon  14829  fuccocl  14866  fucidcl  14867  invfuc  14876  curf2cl  15033  yonedalem4c  15079  yonedalem3  15082  pospo  15135  latjle12  15224  latjlej1  15227  latnlej2  15233  latlem12  15240  latmlem1  15243  latledi  15251  latmlej11  15252  latjass  15257  latj12  15258  latj32  15259  latj13  15260  latj31  15261  latjrot  15262  latjjdi  15265  latjjdir  15266  latdisdlem  15351  prdsmndd  15446  imasmnd2  15450  frmdmnd  15528  grpsubrcan  15598  grpsubadd  15604  grpsubsub  15605  grpaddsubass  15606  grpsubsub4  15609  grpnnncan2  15612  mulgnndir  15640  mulgnn0dir  15641  mulgdir  15643  mulgnnass  15646  mulgnn0ass  15647  mulgass  15648  mulgsubdir  15649  pwsmulg  15660  imasgrp2  15661  issubg2  15687  eqgval  15721  divsgrp  15727  galcan  15813  gacan  15814  oppgmnd  15860  symggrp  15896  pmtrprfv  15950  pmtr3ncom  15972  psgnunilem3  15993  cmn32  16286  cmn12  16288  abladdsub  16295  mulgnn0di  16304  mulgdi  16305  mulgsubdi  16308  dprdss  16516  dprdz  16517  dprdf1o  16519  dprdsn  16523  dprd2da  16531  ablfac1b  16561  pgpfac1lem5  16570  srgi  16603  srgbinomlem2  16629  srgbinom  16633  rngi  16647  prdsrngd  16694  imasrng  16701  opprrng  16713  mulgass3  16719  dvrass  16772  subrgunit  16863  issubrg2  16865  abvdiv  16902  islss3  17020  prdslmodd  17030  islmhm2  17099  lspsolv  17204  islbs2  17215  islbs3  17216  lbsextlem4  17222  sralmod  17248  issubassa  17375  sraassa  17376  psrbaglecl  17417  psrbagcon  17420  psrgrp  17449  psrlmod  17452  psrrng  17463  psrassa  17466  ipdir  18048  ipdi  18049  ipsubdir  18051  ipsubdi  18052  ipass  18054  ipassr  18055  ipassr2  18056  ocvlss  18077  mamudm  18268  matrng  18310  matassa  18311  ofco2  18312  mdetunilem1  18398  mdetunilem9  18406  mdetuni0  18407  mdetmul  18409  gsummatr01lem3  18443  iinopn  18495  subbascn  18838  nrmsep2  18940  isnrm3  18943  regsep2  18960  dnsconst  18962  dfcon2  19003  1stcelcls  19045  nllyidm  19073  dislly  19081  upxp  19176  fbasne0  19383  filss  19406  infil  19416  fsubbas  19420  filssufilg  19464  tmdcn2  19640  psmettri  19867  isxmet2d  19882  xmettri  19906  xmetres2  19916  bldisj  19953  blss2ps  19958  blss2  19959  xmstri2  20021  mstri2  20022  xmstri  20023  mstri  20024  xmstri3  20025  mstri3  20026  msrtri  20027  comet  20068  stdbdbl  20072  met2ndci  20077  ngprcan  20181  ngplcan  20182  ngpsubcan  20185  nrgdsdi  20226  nrgdsdir  20227  nlmdsdi  20242  nlmdsdir  20243  blcvx  20355  icccmplem2  20380  pi1grplem  20601  pi1cof  20611  cvsdiv  20661  cvsdivcl  20662  cphdivcl  20681  cphsubdir  20706  cphsubdi  20707  cphassr  20710  bcthlem5  20819  rrxcph  20876  volfiniun  21008  volcn  21066  itg1val2  21142  dvconst  21371  dvlip  21445  dvfsumlem4  21481  ftc1a  21489  ulmval  21825  ulmdvlem3  21847  ang180  22190  cvxcl  22358  scvxcvx  22359  sgmmul  22520  logexprlim  22544  dchrabl  22573  f1otrge  23086  xmstrkgc  23100  colinearalglem1  23120  colinearalg  23124  axcgrtr  23129  axlowdimlem16  23171  axeuclidlem  23176  axcontlem7  23184  eengtrkg  23199  eengtrkge  23200  wlkoniswlk  23400  constr2trl  23466  wlkdvspth  23475  iseupa  23554  grpodivdiv  23703  grpomuldivass  23704  grpopnpcan2  23708  ablodivdiv4  23746  ablonnncan  23748  ablonnncan1  23750  zerdivemp1  23889  nvmdi  23998  dipassr  24214  archiabllem2c  26180  dvrdir  26226  dvrcan5  26229  kerf1hrm  26260  reofld  26277  pstmfval  26292  tpr2rico  26311  qqhval2lem  26379  qqhvq  26385  issiga  26523  measdivcstOLD  26607  measdivcst  26608  signsply0  26921  erdszelem9  27056  rescon  27104  cvmseu  27134  cvmlift2lem12  27172  cgrid2  28003  segconeu  28011  btwncomim  28013  btwnswapid  28017  cgrxfr  28055  btwnxfr  28056  colineardim1  28061  brofs2  28077  brifs2  28078  idinside  28084  endofsegid  28085  btwnconn1lem7  28093  btwnconn1lem11  28097  btwnconn1  28101  segcon2  28105  seglemin  28113  segletr  28114  btwnsegle  28117  colinbtwnle  28118  broutsideof2  28122  broutsideof3  28126  outsidele  28132  fvray  28141  fvline  28144  linerflx1  28149  ellines  28152  ftc1anc  28446  ivthALT  28501  sdclem1  28610  sstotbnd2  28644  zerdivemp1x  28732  isdrngo2  28735  iscringd  28770  irrapxlem6  29139  jm2.26lem3  29321  dgrsub2  29462  mpaadgr  29482  mendrng  29520  mendlmod  29521  mendassa  29522  fmuldfeq  29735  stoweidlem43  29809  stoweidlem52  29818  stoweidlem53  29819  stoweidlem56  29822  stoweidlem57  29823  el2spthonot0  30361  el2wlkonotot0  30362  usg2wotspth  30374  2pthwlkonot  30375  erclwwlktr  30456  erclwwlkntr  30472  numclwwlk5  30676  friendship  30686  ply1ass23l  30794  linccl  30879  lincext1  30919  lincext3  30921  lincresunit2  30943  bnj149  31797  bnj1118  31904  bnj1128  31910  lsmsat  32546  lfladdcl  32609  lflnegcl  32613  lflvscl  32615  lshpkrlem4  32651  lshpkrlem6  32653  ldualgrplem  32683  lduallmodlem  32690  latmassOLD  32767  latm12  32768  latm32  32769  latmrot  32770  latmmdiN  32772  latmmdir  32773  omlfh1N  32796  omlfh3N  32797  cvlexchb1  32868  cvlexch3  32870  cvlexch4N  32871  cvlatexchb1  32872  cvlsupr2  32881  hlatjass  32907  hlatj12  32908  hlatj32  32909  cvratlem  32958  cvrat  32959  atcvrj0  32965  cvrat2  32966  atltcvr  32972  atexchltN  32978  cvrat3  32979  cvrat4  32980  3dimlem3  32998  3dimlem3OLDN  32999  3at  33027  2atneat  33052  llncmp  33059  2at0mat0  33062  2atmat0  33063  lplnnle2at  33078  llncvrlpln  33095  lplncmp  33099  lplnexllnN  33101  2llnjaN  33103  4atlem11  33146  lplncvrlvol  33153  lvolcmp  33154  2atm2atN  33322  elpaddatriN  33340  paddasslem9  33365  paddass  33375  padd12N  33376  paddssw2  33381  paddss  33382  pmodlem2  33384  pmodN  33387  pmapjlln1  33392  atmod1i1  33394  atmod1i2  33396  pexmidlem2N  33508  pexmidlem6N  33512  pl42N  33520  lhpm0atN  33566  lautlt  33628  lautcvr  33629  lautj  33630  lautm  33631  ltrneq2  33685  cdlemc3  33730  cdlemc4  33731  cdlemd1  33735  cdleme1b  33763  cdleme1  33764  cdleme2  33765  cdleme3e  33769  cdlemefr27cl  33940  cdlemefs27cl  33950  cdleme42mN  34024  cdlemftr2  34103  trljco  34277  tgrpgrplem  34286  tendoplass  34320  tendodi1  34321  tendodi2  34322  cdlemk36  34450  erngdvlem3  34527  erngdvlem3-rN  34535  tendospdi1  34558  dvalveclem  34563  dialss  34584  dvhvaddass  34635  dvhopvsca  34640  dvhlveclem  34646  diblss  34708  diclss  34731  dihmeetlem12N  34856  dihmeetlem15N  34859  dihmeetlem16N  34860  dihmeetlem17N  34861  dihmeetlem18N  34862  dihmeetlem19N  34863  dvh4dimN  34985  lpolvN  35024  lclkr  35071  lclkrs  35077  lcfr  35123
  Copyright terms: Public domain W3C validator