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  715  mptxor  1446  sb4bor  1861  ordsoexmid  4631  eninl  7232  eninr  7233  pw1ne1  7382  negiso  9070  infrenegsupex  9757  xrnegiso  11739  infxrnegsupex  11740  cos01bnd  12235  cos1bnd  12236  cos2bnd  12237  sincos2sgn  12243  sin4lt0  12244  egt2lt3  12257  ssnnctlemct  12983  slotslfn  13024  strslfvd  13040  strslfv2d  13041  strslfv  13043  strslfv3  13044  strsl0  13047  setsslid  13049  setsslnid  13050  rngplusgg  13136  rngmulrg  13137  srngplusgd  13147  srngmulrd  13148  srnginvld  13149  lmodplusgd  13165  lmodscad  13166  lmodvscad  13167  ipsaddgd  13177  ipsmulrd  13178  ipsscad  13179  ipsvscad  13180  ipsipd  13181  topgrpplusgd  13197  topgrptsetd  13198  prdsex  13268  prdsvallem  13271  prdsval  13272  prdssca  13274  prdsmulr  13277  imasex  13304  imasival  13305  imasbas  13306  imasplusg  13307  imasmulr  13308  fnmgp  13851  mgpvalg  13852  mgpex  13854  mgpbasg  13855  mgpscag  13856  mgptsetg  13857  mgpdsg  13859  mgpress  13860  ring1  13988  opprvalg  13998  opprex  14002  opprsllem  14003  rmodislmod  14280  sraval  14366  sralemg  14367  srascag  14371  sravscag  14372  sraipg  14373  sraex  14375  zlmval  14556  zlmlemg  14557  zlmmulrg  14560  zlmsca  14561  zlmvscag  14562  znmul  14571  psrval  14595  fnpsr  14596  setsmsdsg  15119  cosz12  15419  sinpi  15424  sinhalfpilem  15430  coshalfpi  15436  sincosq1lem  15464  tangtx  15477  sincos4thpi  15479  tan4thpi  15480  sincos6thpi  15481  sincos3rdpi  15482  pigt3  15483  logltb  15513  lgsdir2lem4  15675  lgsdir2lem5  15676