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  716  mptxor  1466  sb4bor  1881  ordsoexmid  4653  eninl  7260  eninr  7261  pw1ne1  7410  negiso  9098  infrenegsupex  9785  xrnegiso  11768  infxrnegsupex  11769  cos01bnd  12264  cos1bnd  12265  cos2bnd  12266  sincos2sgn  12272  sin4lt0  12273  egt2lt3  12286  ssnnctlemct  13012  slotslfn  13053  strslfvd  13069  strslfv2d  13070  strslfv  13072  strslfv3  13073  strsl0  13076  setsslid  13078  setsslnid  13079  rngplusgg  13165  rngmulrg  13166  srngplusgd  13176  srngmulrd  13177  srnginvld  13178  lmodplusgd  13194  lmodscad  13195  lmodvscad  13196  ipsaddgd  13206  ipsmulrd  13207  ipsscad  13208  ipsvscad  13209  ipsipd  13210  topgrpplusgd  13226  topgrptsetd  13227  prdsex  13297  prdsvallem  13300  prdsval  13301  prdssca  13303  prdsmulr  13306  imasex  13333  imasival  13334  imasbas  13335  imasplusg  13336  imasmulr  13337  fnmgp  13880  mgpvalg  13881  mgpex  13883  mgpbasg  13884  mgpscag  13885  mgptsetg  13886  mgpdsg  13888  mgpress  13889  ring1  14017  opprvalg  14027  opprex  14031  opprsllem  14032  rmodislmod  14309  sraval  14395  sralemg  14396  srascag  14400  sravscag  14401  sraipg  14402  sraex  14404  zlmval  14585  zlmlemg  14586  zlmmulrg  14589  zlmsca  14590  zlmvscag  14591  znmul  14600  psrval  14624  fnpsr  14625  setsmsdsg  15148  cosz12  15448  sinpi  15453  sinhalfpilem  15459  coshalfpi  15465  sincosq1lem  15493  tangtx  15506  sincos4thpi  15508  tan4thpi  15509  sincos6thpi  15510  sincos3rdpi  15511  pigt3  15512  logltb  15542  lgsdir2lem4  15704  lgsdir2lem5  15705