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  712  mptxor  1443  sb4bor  1857  ordsoexmid  4609  eninl  7198  eninr  7199  pw1ne1  7340  negiso  9027  infrenegsupex  9714  xrnegiso  11515  infxrnegsupex  11516  cos01bnd  12011  cos1bnd  12012  cos2bnd  12013  sincos2sgn  12019  sin4lt0  12020  egt2lt3  12033  ssnnctlemct  12759  slotslfn  12800  strslfvd  12816  strslfv2d  12817  strslfv  12819  strslfv3  12820  strsl0  12823  setsslid  12825  setsslnid  12826  rngplusgg  12911  rngmulrg  12912  srngplusgd  12922  srngmulrd  12923  srnginvld  12924  lmodplusgd  12940  lmodscad  12941  lmodvscad  12942  ipsaddgd  12952  ipsmulrd  12953  ipsscad  12954  ipsvscad  12955  ipsipd  12956  topgrpplusgd  12972  topgrptsetd  12973  prdsex  13043  prdsvallem  13046  prdsval  13047  prdssca  13049  prdsmulr  13052  imasex  13079  imasival  13080  imasbas  13081  imasplusg  13082  imasmulr  13083  fnmgp  13626  mgpvalg  13627  mgpex  13629  mgpbasg  13630  mgpscag  13631  mgptsetg  13632  mgpdsg  13634  mgpress  13635  ring1  13763  opprvalg  13773  opprex  13777  opprsllem  13778  rmodislmod  14055  sraval  14141  sralemg  14142  srascag  14146  sravscag  14147  sraipg  14148  sraex  14150  zlmval  14331  zlmlemg  14332  zlmmulrg  14335  zlmsca  14336  zlmvscag  14337  znmul  14346  psrval  14370  fnpsr  14371  setsmsdsg  14894  cosz12  15194  sinpi  15199  sinhalfpilem  15205  coshalfpi  15211  sincosq1lem  15239  tangtx  15252  sincos4thpi  15254  tan4thpi  15255  sincos6thpi  15256  sincos3rdpi  15257  pigt3  15258  logltb  15288  lgsdir2lem4  15450  lgsdir2lem5  15451