Theorem simpri 113

Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)

Hypothesis

Ref	Expression
simpri.1	|- ( ph /\ ps )

Assertion

Ref	Expression
simpri	|- ps

Proof of Theorem simpri

Step	Hyp	Ref	Expression
1		simpri.1	. 2 |- ( ph /\ ps )
2		simpr 110	. 2 |- ( ( ph /\ ps ) -> ps )
3	1, 2	ax-mp 5	1 |- ps

Syntax hints:   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-ia2 107

This theorem is referenced by:  bi3  119  dfbi2  388  olc  712  mptxor  1435  sb4bor  1849  ordsoexmid  4598  eninl  7163  eninr  7164  pw1ne1  7296  negiso  8982  infrenegsupex  9668  xrnegiso  11427  infxrnegsupex  11428  cos01bnd  11923  cos1bnd  11924  cos2bnd  11925  sincos2sgn  11931  sin4lt0  11932  egt2lt3  11945  ssnnctlemct  12663  slotslfn  12704  strslfvd  12720  strslfv2d  12721  strslfv  12723  strsl0  12727  setsslid  12729  setsslnid  12730  rngplusgg  12814  rngmulrg  12815  srngplusgd  12825  srngmulrd  12826  srnginvld  12827  lmodplusgd  12843  lmodscad  12844  lmodvscad  12845  ipsaddgd  12855  ipsmulrd  12856  ipsscad  12857  ipsvscad  12858  ipsipd  12859  topgrpplusgd  12875  topgrptsetd  12876  prdsex  12940  imasex  12948  imasival  12949  imasbas  12950  imasplusg  12951  imasmulr  12952  fnmgp  13478  mgpvalg  13479  mgpex  13481  mgpbasg  13482  mgpscag  13483  mgptsetg  13484  mgpdsg  13486  mgpress  13487  ring1  13615  opprvalg  13625  opprex  13629  opprsllem  13630  rmodislmod  13907  sraval  13993  sralemg  13994  srascag  13998  sravscag  13999  sraipg  14000  sraex  14002  zlmval  14183  zlmlemg  14184  zlmmulrg  14187  zlmsca  14188  zlmvscag  14189  znmul  14198  psrval  14220  fnpsr  14221  setsmsdsg  14716  cosz12  15016  sinpi  15021  sinhalfpilem  15027  coshalfpi  15033  sincosq1lem  15061  tangtx  15074  sincos4thpi  15076  tan4thpi  15077  sincos6thpi  15078  sincos3rdpi  15079  pigt3  15080  logltb  15110  lgsdir2lem4  15272  lgsdir2lem5  15273