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  392  olc  723  mptxor  1473  sb4bor  1888  ordsoexmid  4704  eninl  7427  eninr  7428  pw1ne1  7578  negiso  9275  infrenegsupex  9973  xrnegiso  12006  infxrnegsupex  12007  cos01bnd  12503  cos1bnd  12504  cos2bnd  12505  sincos2sgn  12511  sin4lt0  12512  egt2lt3  12525  ssnnctlemct  13315  slotslfn  13356  strslfvd  13372  strslfv2d  13373  strslfv  13375  strslfv3  13376  strsl0  13379  setsslid  13381  setsslnid  13382  rngplusgg  13468  rngmulrg  13469  srngplusgd  13479  srngmulrd  13480  srnginvld  13481  lmodplusgd  13497  lmodscad  13498  lmodvscad  13499  ipsaddgd  13509  ipsmulrd  13510  ipsscad  13511  ipsvscad  13512  ipsipd  13513  topgrpplusgd  13529  topgrptsetd  13530  prdsvallem  13598  imasex  13603  imasival  13604  imasbas  13605  imasplusg  13606  imasmulr  13607  prdsex  14149  prdsval  14150  prdssca  14152  prdsmulr  14155  fnmgp  14196  mgpvalg  14197  mgpex  14199  mgpbasg  14200  mgpscag  14201  mgptsetg  14202  mgpdsg  14204  mgpress  14205  ring1  14337  opprvalg  14347  opprex  14351  opprsllem  14352  rmodislmod  14660  sraval  14746  sralemg  14747  srascag  14751  sravscag  14752  sraipg  14753  sraex  14755  zlmval  14934  zlmlemg  14935  zlmmulrg  14938  zlmsca  14939  zlmvscag  14940  znmul  14949  psrval  14973  fnpsr  14974  setsmsdsg  15504  cosz12  15804  sinpi  15809  sinhalfpilem  15815  coshalfpi  15821  sincosq1lem  15849  tangtx  15862  sincos4thpi  15864  tan4thpi  15865  sincos6thpi  15866  sincos3rdpi  15867  pigt3  15868  logltb  15898  lgsdir2lem4  16064  lgsdir2lem5  16065