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  4689  eninl  7401  eninr  7402  pw1ne1  7552  negiso  9246  infrenegsupex  9944  xrnegiso  11972  infxrnegsupex  11973  cos01bnd  12469  cos1bnd  12470  cos2bnd  12471  sincos2sgn  12477  sin4lt0  12478  egt2lt3  12491  ssnnctlemct  13281  slotslfn  13322  strslfvd  13338  strslfv2d  13339  strslfv  13341  strslfv3  13342  strsl0  13345  setsslid  13347  setsslnid  13348  rngplusgg  13434  rngmulrg  13435  srngplusgd  13445  srngmulrd  13446  srnginvld  13447  lmodplusgd  13463  lmodscad  13464  lmodvscad  13465  ipsaddgd  13475  ipsmulrd  13476  ipsscad  13477  ipsvscad  13478  ipsipd  13479  topgrpplusgd  13495  topgrptsetd  13496  prdsvallem  13564  imasex  13569  imasival  13570  imasbas  13571  imasplusg  13572  imasmulr  13573  prdsex  14114  prdsval  14115  prdssca  14117  prdsmulr  14120  fnmgp  14161  mgpvalg  14162  mgpex  14164  mgpbasg  14165  mgpscag  14166  mgptsetg  14167  mgpdsg  14169  mgpress  14170  ring1  14302  opprvalg  14312  opprex  14316  opprsllem  14317  rmodislmod  14625  sraval  14711  sralemg  14712  srascag  14716  sravscag  14717  sraipg  14718  sraex  14720  zlmval  14901  zlmlemg  14902  zlmmulrg  14905  zlmsca  14906  zlmvscag  14907  znmul  14916  psrval  14940  fnpsr  14941  setsmsdsg  15471  cosz12  15771  sinpi  15776  sinhalfpilem  15782  coshalfpi  15788  sincosq1lem  15816  tangtx  15829  sincos4thpi  15831  tan4thpi  15832  sincos6thpi  15833  sincos3rdpi  15834  pigt3  15835  logltb  15865  lgsdir2lem4  16030  lgsdir2lem5  16031