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  718  mptxor  1468  sb4bor  1883  ordsoexmid  4660  eninl  7295  eninr  7296  pw1ne1  7446  negiso  9134  infrenegsupex  9827  xrnegiso  11822  infxrnegsupex  11823  cos01bnd  12318  cos1bnd  12319  cos2bnd  12320  sincos2sgn  12326  sin4lt0  12327  egt2lt3  12340  ssnnctlemct  13066  slotslfn  13107  strslfvd  13123  strslfv2d  13124  strslfv  13126  strslfv3  13127  strsl0  13130  setsslid  13132  setsslnid  13133  rngplusgg  13219  rngmulrg  13220  srngplusgd  13230  srngmulrd  13231  srnginvld  13232  lmodplusgd  13248  lmodscad  13249  lmodvscad  13250  ipsaddgd  13260  ipsmulrd  13261  ipsscad  13262  ipsvscad  13263  ipsipd  13264  topgrpplusgd  13280  topgrptsetd  13281  prdsex  13351  prdsvallem  13354  prdsval  13355  prdssca  13357  prdsmulr  13360  imasex  13387  imasival  13388  imasbas  13389  imasplusg  13390  imasmulr  13391  fnmgp  13934  mgpvalg  13935  mgpex  13937  mgpbasg  13938  mgpscag  13939  mgptsetg  13940  mgpdsg  13942  mgpress  13943  ring1  14071  opprvalg  14081  opprex  14085  opprsllem  14086  rmodislmod  14364  sraval  14450  sralemg  14451  srascag  14455  sravscag  14456  sraipg  14457  sraex  14459  zlmval  14640  zlmlemg  14641  zlmmulrg  14644  zlmsca  14645  zlmvscag  14646  znmul  14655  psrval  14679  fnpsr  14680  setsmsdsg  15203  cosz12  15503  sinpi  15508  sinhalfpilem  15514  coshalfpi  15520  sincosq1lem  15548  tangtx  15561  sincos4thpi  15563  tan4thpi  15564  sincos6thpi  15565  sincos3rdpi  15566  pigt3  15567  logltb  15597  lgsdir2lem4  15759  lgsdir2lem5  15760