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  10010  xrnegiso  12053  infxrnegsupex  12054  cos01bnd  12550  cos1bnd  12551  cos2bnd  12552  sincos2sgn  12558  sin4lt0  12559  egt2lt3  12572  ssnnctlemct  13395  slotslfn  13436  strslfvd  13452  strslfv2d  13453  strslfv  13455  strslfv3  13456  strsl0  13459  setsslid  13461  setsslnid  13462  slotm  13473  rngplusgg  13550  rngmulrg  13551  srngplusgd  13561  srngmulrd  13562  srnginvld  13563  lmodplusgd  13579  lmodscad  13580  lmodvscad  13581  ipsaddgd  13591  ipsmulrd  13592  ipsscad  13593  ipsvscad  13594  ipsipd  13595  topgrpplusgd  13611  topgrptsetd  13612  prdsvallem  13680  imasex  13685  imasival  13686  imasbas  13687  imasplusg  13688  imasmulr  13689  prdsex  14279  prdsval  14280  prdssca  14282  prdsmulr  14285  fnmgp  14326  mgpvalg  14327  mgpex  14330  mgpbasg  14331  mgpscag  14333  mgptsetg  14334  mgpdsg  14336  mgpress  14337  ring1  14471  opprvalg  14483  opprex  14487  opprsllem  14488  rmodislmod  14797  sraval  14883  sralemg  14884  srascag  14888  sravscag  14889  sraipg  14890  sraex  14892  zlmval  15071  zlmlemg  15072  zlmmulrg  15075  zlmsca  15076  zlmvscag  15077  znmul  15086  psrval  15159  fnpsr  15160  setsmsdsg  15706  cosz12  16007  sinpi  16012  sinhalfpilem  16018  coshalfpi  16024  sincosq1lem  16052  tangtx  16065  sincos4thpi  16067  tan4thpi  16068  sincos6thpi  16069  sincos3rdpi  16070  pigt3  16071  logltb  16104  log2tlbndlog2  16220  ppiublem1  16291  ppiublem2  16292  bposlem9  16319  lgsdir2lem4  16355  lgsdir2lem5  16356