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

Theorem simpr1 1002
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 996 . 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 973
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 975
This theorem is referenced by:  simplr1  1038  simprr1  1044  simp1r1  1092  simp2r1  1098  simp3r1  1104  3anandis  1330  isopolem  6227  fr3nr  6593  suppfnss  6922  frfi  7761  intrnfi  7872  iinfi  7873  eqsup  7912  fisupcl  7923  cnfcomlem  8139  cnfcomlemOLD  8147  ackbij1lem15  8610  fpwwe2lem5  9008  dedekindle  9740  ico0  11571  elioc2  11583  elico2  11584  elicc2  11585  iccsplit  11649  fseq1p1m1  11748  elfz0ubfz0  11772  hashtpg  12485  swrdsymbeq  12631  ccatswrd  12640  tanadd  13759  dvds2ln  13871  qredeq  14102  ressress  14548  mreexexlem4d  14898  mreexexd  14899  0catg  14938  2oppccomf  14977  issubc3  15072  fthmon  15150  fuccocl  15187  fucidcl  15188  invfuc  15197  curf2cl  15354  yonedalem4c  15400  yonedalem3  15403  pospo  15456  latjle12  15545  latjlej1  15548  latnlej2  15554  latlem12  15561  latmlem1  15564  latledi  15572  latmlej11  15573  latjass  15578  latj12  15579  latj32  15580  latj13  15581  latj31  15582  latjrot  15583  latjjdi  15586  latjjdir  15587  latdisdlem  15672  prdsmndd  15767  imasmnd2  15771  frmdmnd  15850  grpsubrcan  15920  grpsubadd  15927  grpsubsub  15928  grpaddsubass  15929  grpsubsub4  15932  grpnnncan2  15936  mulgnndir  15964  mulgnn0dir  15965  mulgdir  15967  mulgnnass  15970  mulgnn0ass  15971  mulgass  15972  mulgsubdir  15973  pwsmulg  15984  imasgrp2  15985  issubg2  16011  eqgval  16045  divsgrp  16051  galcan  16137  gacan  16138  oppgmnd  16184  symggrp  16220  pmtrprfv  16274  pmtr3ncom  16296  psgnunilem3  16317  cmn32  16612  cmn12  16614  abladdsub  16621  mulgnn0di  16630  mulgdi  16631  mulgsubdi  16634  dprdss  16866  dprdz  16867  dprdf1o  16869  dprdsn  16873  dprd2da  16881  ablfac1b  16911  pgpfac1lem5  16920  srgi  16953  srgbinomlem2  16980  srgbinom  16984  rngi  16998  prdsrngd  17045  imasrng  17052  opprrng  17064  mulgass3  17070  dvrass  17123  kerf1hrm  17175  subrgunit  17230  issubrg2  17232  abvdiv  17269  islss3  17388  prdslmodd  17398  islmhm2  17467  lspsolv  17572  islbs2  17583  islbs3  17584  lbsextlem4  17590  sralmod  17616  issubassa  17744  sraassa  17745  psrbaglecl  17790  psrbagcon  17793  psrgrp  17822  psrlmod  17825  psrrng  17837  psrassa  17840  ipdir  18441  ipdi  18442  ipsubdir  18444  ipsubdi  18445  ipass  18447  ipassr  18448  ipassr2  18449  ocvlss  18470  mamudm  18657  matrng  18712  matassa  18713  ofco2  18720  mdetunilem1  18881  mdetunilem9  18889  mdetuni0  18890  mdetmul  18892  gsummatr01lem3  18926  iinopn  19178  subbascn  19521  nrmsep2  19623  isnrm3  19626  regsep2  19643  dnsconst  19645  dfcon2  19686  1stcelcls  19728  nllyidm  19756  dislly  19764  upxp  19859  fbasne0  20066  filss  20089  infil  20099  fsubbas  20103  filssufilg  20147  tmdcn2  20323  psmettri  20550  isxmet2d  20565  xmettri  20589  xmetres2  20599  bldisj  20636  blss2ps  20641  blss2  20642  xmstri2  20704  mstri2  20705  xmstri  20706  mstri  20707  xmstri3  20708  mstri3  20709  msrtri  20710  comet  20751  stdbdbl  20755  met2ndci  20760  ngprcan  20864  ngplcan  20865  ngpsubcan  20868  nrgdsdi  20909  nrgdsdir  20910  nlmdsdi  20925  nlmdsdir  20926  blcvx  21038  icccmplem2  21063  pi1grplem  21284  pi1cof  21294  cvsdiv  21344  cvsdivcl  21345  cphdivcl  21364  cphsubdir  21389  cphsubdi  21390  cphassr  21393  bcthlem5  21502  rrxcph  21559  volfiniun  21692  volcn  21750  itg1val2  21826  dvconst  22055  dvlip  22129  dvfsumlem4  22165  ftc1a  22173  ulmval  22509  ulmdvlem3  22531  ang180  22874  cvxcl  23042  scvxcvx  23043  sgmmul  23204  logexprlim  23228  dchrabl  23257  motgrp  23658  f1otrge  23851  xmstrkgc  23865  colinearalglem1  23885  colinearalg  23889  axcgrtr  23894  axlowdimlem16  23936  axeuclidlem  23941  axcontlem7  23949  eengtrkg  23964  eengtrkge  23965  wlkoniswlk  24212  constr2trl  24277  wlkdvspth  24286  erclwwlktr  24491  erclwwlkntr  24503  el2spthonot0  24547  el2wlkonotot0  24548  usg2wotspth  24560  2pthwlkonot  24561  iseupa  24641  numclwwlk5  24789  friendship  24799  grpodivdiv  24926  grpomuldivass  24927  grpopnpcan2  24931  ablodivdiv4  24969  ablonnncan  24971  ablonnncan1  24973  zerdivemp1  25112  nvmdi  25221  dipassr  25437  archiabllem2c  27401  dvrdir  27443  dvrcan5  27446  reofld  27493  pstmfval  27511  tpr2rico  27530  qqhval2lem  27598  qqhvq  27604  issiga  27751  measdivcstOLD  27835  measdivcst  27836  signsply0  28148  erdszelem9  28283  rescon  28331  cvmseu  28361  cvmlift2lem12  28399  cgrid2  29230  segconeu  29238  btwncomim  29240  btwnswapid  29244  cgrxfr  29282  btwnxfr  29283  colineardim1  29288  brofs2  29304  brifs2  29305  idinside  29311  endofsegid  29312  btwnconn1lem7  29320  btwnconn1lem11  29324  btwnconn1  29328  segcon2  29332  seglemin  29340  segletr  29341  btwnsegle  29344  colinbtwnle  29345  broutsideof2  29349  broutsideof3  29353  outsidele  29359  fvray  29368  fvline  29371  linerflx1  29376  ellines  29379  ftc1anc  29675  ivthALT  29730  sdclem1  29839  sstotbnd2  29873  zerdivemp1x  29961  isdrngo2  29964  iscringd  29999  irrapxlem6  30367  jm2.26lem3  30547  dgrsub2  30688  mpaadgr  30708  mendrng  30746  mendlmod  30747  mendassa  30748  fmuldfeq  31133  stoweidlem43  31343  stoweidlem52  31352  stoweidlem53  31353  stoweidlem56  31356  stoweidlem57  31357  usgfis  31915  usgfisALT  31919  ply1ass23l  32055  linccl  32088  lincext1  32128  lincext3  32130  lincresunit2  32152  bnj149  33012  bnj1118  33119  bnj1128  33125  lsmsat  33805  lfladdcl  33868  lflnegcl  33872  lflvscl  33874  lshpkrlem4  33910  lshpkrlem6  33912  ldualgrplem  33942  lduallmodlem  33949  latmassOLD  34026  latm12  34027  latm32  34028  latmrot  34029  latmmdiN  34031  latmmdir  34032  omlfh1N  34055  omlfh3N  34056  cvlexchb1  34127  cvlexch3  34129  cvlexch4N  34130  cvlatexchb1  34131  cvlsupr2  34140  hlatjass  34166  hlatj12  34167  hlatj32  34168  cvratlem  34217  cvrat  34218  atcvrj0  34224  cvrat2  34225  atltcvr  34231  atexchltN  34237  cvrat3  34238  cvrat4  34239  3dimlem3  34257  3dimlem3OLDN  34258  3at  34286  2atneat  34311  llncmp  34318  2at0mat0  34321  2atmat0  34322  lplnnle2at  34337  llncvrlpln  34354  lplncmp  34358  lplnexllnN  34360  2llnjaN  34362  4atlem11  34405  lplncvrlvol  34412  lvolcmp  34413  2atm2atN  34581  elpaddatriN  34599  paddasslem9  34624  paddass  34634  padd12N  34635  paddssw2  34640  paddss  34641  pmodlem2  34643  pmodN  34646  pmapjlln1  34651  atmod1i1  34653  atmod1i2  34655  pexmidlem2N  34767  pexmidlem6N  34771  pl42N  34779  lhpm0atN  34825  lautlt  34887  lautcvr  34888  lautj  34889  lautm  34890  ltrneq2  34944  cdlemc3  34989  cdlemc4  34990  cdlemd1  34994  cdleme1b  35022  cdleme1  35023  cdleme2  35024  cdleme3e  35028  cdlemefr27cl  35199  cdlemefs27cl  35209  cdleme42mN  35283  cdlemftr2  35362  trljco  35536  tgrpgrplem  35545  tendoplass  35579  tendodi1  35580  tendodi2  35581  cdlemk36  35709  erngdvlem3  35786  erngdvlem3-rN  35794  tendospdi1  35817  dvalveclem  35822  dialss  35843  dvhvaddass  35894  dvhopvsca  35899  dvhlveclem  35905  diblss  35967  diclss  35990  dihmeetlem12N  36115  dihmeetlem15N  36118  dihmeetlem16N  36119  dihmeetlem17N  36120  dihmeetlem18N  36121  dihmeetlem19N  36122  dvh4dimN  36244  lpolvN  36283  lclkr  36330  lclkrs  36336  lcfr  36382
  Copyright terms: Public domain W3C validator