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  716  mptxor  1466  sb4bor  1881  ordsoexmid  4654  eninl  7275  eninr  7276  pw1ne1  7425  negiso  9113  infrenegsupex  9801  xrnegiso  11788  infxrnegsupex  11789  cos01bnd  12284  cos1bnd  12285  cos2bnd  12286  sincos2sgn  12292  sin4lt0  12293  egt2lt3  12306  ssnnctlemct  13032  slotslfn  13073  strslfvd  13089  strslfv2d  13090  strslfv  13092  strslfv3  13093  strsl0  13096  setsslid  13098  setsslnid  13099  rngplusgg  13185  rngmulrg  13186  srngplusgd  13196  srngmulrd  13197  srnginvld  13198  lmodplusgd  13214  lmodscad  13215  lmodvscad  13216  ipsaddgd  13226  ipsmulrd  13227  ipsscad  13228  ipsvscad  13229  ipsipd  13230  topgrpplusgd  13246  topgrptsetd  13247  prdsex  13317  prdsvallem  13320  prdsval  13321  prdssca  13323  prdsmulr  13326  imasex  13353  imasival  13354  imasbas  13355  imasplusg  13356  imasmulr  13357  fnmgp  13900  mgpvalg  13901  mgpex  13903  mgpbasg  13904  mgpscag  13905  mgptsetg  13906  mgpdsg  13908  mgpress  13909  ring1  14037  opprvalg  14047  opprex  14051  opprsllem  14052  rmodislmod  14330  sraval  14416  sralemg  14417  srascag  14421  sravscag  14422  sraipg  14423  sraex  14425  zlmval  14606  zlmlemg  14607  zlmmulrg  14610  zlmsca  14611  zlmvscag  14612  znmul  14621  psrval  14645  fnpsr  14646  setsmsdsg  15169  cosz12  15469  sinpi  15474  sinhalfpilem  15480  coshalfpi  15486  sincosq1lem  15514  tangtx  15527  sincos4thpi  15529  tan4thpi  15530  sincos6thpi  15531  sincos3rdpi  15532  pigt3  15533  logltb  15563  lgsdir2lem4  15725  lgsdir2lem5  15726