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

This proof depends on syntax axioms:   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-ia2 107

This theorem is used by:  bi3  119  dfbi2  392  olc  723  mptxor  1473  sb4bor  1888  ordsoexmid  4711  eninl  7443  eninr  7444  pw1ne1  7594  negiso  9293  infrenegsupex  10009  xrnegiso  12052  infxrnegsupex  12053  cos01bnd  12549  cos1bnd  12550  cos2bnd  12551  sincos2sgn  12557  sin4lt0  12558  egt2lt3  12571  ssnnctlemct  13394  slotslfn  13435  strslfvd  13451  strslfv2d  13452  strslfv  13454  strslfv3  13455  strsl0  13458  setsslid  13460  setsslnid  13461  slotm  13472  rngplusgg  13549  rngmulrg  13550  srngplusgd  13560  srngmulrd  13561  srnginvld  13562  lmodplusgd  13578  lmodscad  13579  lmodvscad  13580  ipsaddgd  13590  ipsmulrd  13591  ipsscad  13592  ipsvscad  13593  ipsipd  13594  topgrpplusgd  13610  topgrptsetd  13611  prdsvallem  13679  imasex  13684  imasival  13685  imasbas  13686  imasplusg  13687  imasmulr  13688  prdsex  14278  prdsval  14279  prdssca  14281  prdsmulr  14284  fnmgp  14325  mgpvalg  14326  mgpex  14329  mgpbasg  14330  mgpscag  14332  mgptsetg  14333  mgpdsg  14335  mgpress  14336  ring1  14470  opprvalg  14482  opprex  14486  opprsllem  14487  rmodislmod  14796  sraval  14882  sralemg  14883  srascag  14887  sravscag  14888  sraipg  14889  sraex  14891  zlmval  15070  zlmlemg  15071  zlmmulrg  15074  zlmsca  15075  zlmvscag  15076  znmul  15085  psrval  15160  fnpsr  15161  setsmsdsg  15723  cosz12  16024  sinpi  16029  sinhalfpilem  16035  coshalfpi  16041  sincosq1lem  16069  tangtx  16082  sincos4thpi  16084  tan4thpi  16085  sincos6thpi  16086  sincos3rdpi  16087  pigt3  16088  logltb  16121  log2tlbndlog2  16237  ppiublem1  16308  ppiublem2  16309  bposlem9  16336  lgsdir2lem4  16372  lgsdir2lem5  16373