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  4658  eninl  7287  eninr  7288  pw1ne1  7437  negiso  9125  infrenegsupex  9818  xrnegiso  11813  infxrnegsupex  11814  cos01bnd  12309  cos1bnd  12310  cos2bnd  12311  sincos2sgn  12317  sin4lt0  12318  egt2lt3  12331  ssnnctlemct  13057  slotslfn  13098  strslfvd  13114  strslfv2d  13115  strslfv  13117  strslfv3  13118  strsl0  13121  setsslid  13123  setsslnid  13124  rngplusgg  13210  rngmulrg  13211  srngplusgd  13221  srngmulrd  13222  srnginvld  13223  lmodplusgd  13239  lmodscad  13240  lmodvscad  13241  ipsaddgd  13251  ipsmulrd  13252  ipsscad  13253  ipsvscad  13254  ipsipd  13255  topgrpplusgd  13271  topgrptsetd  13272  prdsex  13342  prdsvallem  13345  prdsval  13346  prdssca  13348  prdsmulr  13351  imasex  13378  imasival  13379  imasbas  13380  imasplusg  13381  imasmulr  13382  fnmgp  13925  mgpvalg  13926  mgpex  13928  mgpbasg  13929  mgpscag  13930  mgptsetg  13931  mgpdsg  13933  mgpress  13934  ring1  14062  opprvalg  14072  opprex  14076  opprsllem  14077  rmodislmod  14355  sraval  14441  sralemg  14442  srascag  14446  sravscag  14447  sraipg  14448  sraex  14450  zlmval  14631  zlmlemg  14632  zlmmulrg  14635  zlmsca  14636  zlmvscag  14637  znmul  14646  psrval  14670  fnpsr  14671  setsmsdsg  15194  cosz12  15494  sinpi  15499  sinhalfpilem  15505  coshalfpi  15511  sincosq1lem  15539  tangtx  15552  sincos4thpi  15554  tan4thpi  15555  sincos6thpi  15556  sincos3rdpi  15557  pigt3  15558  logltb  15588  lgsdir2lem4  15750  lgsdir2lem5  15751