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  719  mptxor  1469  sb4bor  1884  ordsoexmid  4684  eninl  7388  eninr  7389  pw1ne1  7539  negiso  9229  infrenegsupex  9926  xrnegiso  11947  infxrnegsupex  11948  cos01bnd  12444  cos1bnd  12445  cos2bnd  12446  sincos2sgn  12452  sin4lt0  12453  egt2lt3  12466  ssnnctlemct  13197  slotslfn  13238  strslfvd  13254  strslfv2d  13255  strslfv  13257  strslfv3  13258  strsl0  13261  setsslid  13263  setsslnid  13264  rngplusgg  13350  rngmulrg  13351  srngplusgd  13361  srngmulrd  13362  srnginvld  13363  lmodplusgd  13379  lmodscad  13380  lmodvscad  13381  ipsaddgd  13391  ipsmulrd  13392  ipsscad  13393  ipsvscad  13394  ipsipd  13395  topgrpplusgd  13411  topgrptsetd  13412  prdsex  13482  prdsvallem  13485  prdsval  13486  prdssca  13488  prdsmulr  13491  imasex  13518  imasival  13519  imasbas  13520  imasplusg  13521  imasmulr  13522  fnmgp  14066  mgpvalg  14067  mgpex  14069  mgpbasg  14070  mgpscag  14071  mgptsetg  14072  mgpdsg  14074  mgpress  14075  ring1  14203  opprvalg  14213  opprex  14217  opprsllem  14218  rmodislmod  14499  sraval  14585  sralemg  14586  srascag  14590  sravscag  14591  sraipg  14592  sraex  14594  zlmval  14775  zlmlemg  14776  zlmmulrg  14779  zlmsca  14780  zlmvscag  14781  znmul  14790  psrval  14814  fnpsr  14815  setsmsdsg  15345  cosz12  15645  sinpi  15650  sinhalfpilem  15656  coshalfpi  15662  sincosq1lem  15690  tangtx  15703  sincos4thpi  15705  tan4thpi  15706  sincos6thpi  15707  sincos3rdpi  15708  pigt3  15709  logltb  15739  lgsdir2lem4  15904  lgsdir2lem5  15905