Theorem simpri 113

Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)

Hypothesis

Ref	Expression
simpri.1	⊢ (𝜑 ∧ 𝜓)

Assertion

Ref	Expression
simpri	⊢ 𝜓

Proof of Theorem simpri

Step	Hyp	Ref	Expression
1		simpri.1	. 2 ⊢ (𝜑 ∧ 𝜓)
2		simpr 110	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3	1, 2	ax-mp 5	1 ⊢ 𝜓

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  719  mptxor  1469  sb4bor  1884  ordsoexmid  4689  eninl  7401  eninr  7402  pw1ne1  7552  negiso  9249  infrenegsupex  9947  xrnegiso  11975  infxrnegsupex  11976  cos01bnd  12472  cos1bnd  12473  cos2bnd  12474  sincos2sgn  12480  sin4lt0  12481  egt2lt3  12494  ssnnctlemct  13284  slotslfn  13325  strslfvd  13341  strslfv2d  13342  strslfv  13344  strslfv3  13345  strsl0  13348  setsslid  13350  setsslnid  13351  rngplusgg  13437  rngmulrg  13438  srngplusgd  13448  srngmulrd  13449  srnginvld  13450  lmodplusgd  13466  lmodscad  13467  lmodvscad  13468  ipsaddgd  13478  ipsmulrd  13479  ipsscad  13480  ipsvscad  13481  ipsipd  13482  topgrpplusgd  13498  topgrptsetd  13499  prdsvallem  13567  imasex  13572  imasival  13573  imasbas  13574  imasplusg  13575  imasmulr  13576  prdsex  14117  prdsval  14118  prdssca  14120  prdsmulr  14123  fnmgp  14164  mgpvalg  14165  mgpex  14167  mgpbasg  14168  mgpscag  14169  mgptsetg  14170  mgpdsg  14172  mgpress  14173  ring1  14305  opprvalg  14315  opprex  14319  opprsllem  14320  rmodislmod  14628  sraval  14714  sralemg  14715  srascag  14719  sravscag  14720  sraipg  14721  sraex  14723  zlmval  14904  zlmlemg  14905  zlmmulrg  14908  zlmsca  14909  zlmvscag  14910  znmul  14919  psrval  14943  fnpsr  14944  setsmsdsg  15474  cosz12  15774  sinpi  15779  sinhalfpilem  15785  coshalfpi  15791  sincosq1lem  15819  tangtx  15832  sincos4thpi  15834  tan4thpi  15835  sincos6thpi  15836  sincos3rdpi  15837  pigt3  15838  logltb  15868  lgsdir2lem4  16033  lgsdir2lem5  16034