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  1883  ordsoexmid  4666  eninl  7339  eninr  7340  pw1ne1  7490  negiso  9177  infrenegsupex  9872  xrnegiso  11885  infxrnegsupex  11886  cos01bnd  12382  cos1bnd  12383  cos2bnd  12384  sincos2sgn  12390  sin4lt0  12391  egt2lt3  12404  ssnnctlemct  13130  slotslfn  13171  strslfvd  13187  strslfv2d  13188  strslfv  13190  strslfv3  13191  strsl0  13194  setsslid  13196  setsslnid  13197  rngplusgg  13283  rngmulrg  13284  srngplusgd  13294  srngmulrd  13295  srnginvld  13296  lmodplusgd  13312  lmodscad  13313  lmodvscad  13314  ipsaddgd  13324  ipsmulrd  13325  ipsscad  13326  ipsvscad  13327  ipsipd  13328  topgrpplusgd  13344  topgrptsetd  13345  prdsex  13415  prdsvallem  13418  prdsval  13419  prdssca  13421  prdsmulr  13424  imasex  13451  imasival  13452  imasbas  13453  imasplusg  13454  imasmulr  13455  fnmgp  13999  mgpvalg  14000  mgpex  14002  mgpbasg  14003  mgpscag  14004  mgptsetg  14005  mgpdsg  14007  mgpress  14008  ring1  14136  opprvalg  14146  opprex  14150  opprsllem  14151  rmodislmod  14430  sraval  14516  sralemg  14517  srascag  14521  sravscag  14522  sraipg  14523  sraex  14525  zlmval  14706  zlmlemg  14707  zlmmulrg  14710  zlmsca  14711  zlmvscag  14712  znmul  14721  psrval  14745  fnpsr  14746  setsmsdsg  15274  cosz12  15574  sinpi  15579  sinhalfpilem  15585  coshalfpi  15591  sincosq1lem  15619  tangtx  15632  sincos4thpi  15634  tan4thpi  15635  sincos6thpi  15636  sincos3rdpi  15637  pigt3  15638  logltb  15668  lgsdir2lem4  15833  lgsdir2lem5  15834