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  713  mptxor  1444  sb4bor  1859  ordsoexmid  4614  eninl  7206  eninr  7207  pw1ne1  7348  negiso  9035  infrenegsupex  9722  xrnegiso  11617  infxrnegsupex  11618  cos01bnd  12113  cos1bnd  12114  cos2bnd  12115  sincos2sgn  12121  sin4lt0  12122  egt2lt3  12135  ssnnctlemct  12861  slotslfn  12902  strslfvd  12918  strslfv2d  12919  strslfv  12921  strslfv3  12922  strsl0  12925  setsslid  12927  setsslnid  12928  rngplusgg  13013  rngmulrg  13014  srngplusgd  13024  srngmulrd  13025  srnginvld  13026  lmodplusgd  13042  lmodscad  13043  lmodvscad  13044  ipsaddgd  13054  ipsmulrd  13055  ipsscad  13056  ipsvscad  13057  ipsipd  13058  topgrpplusgd  13074  topgrptsetd  13075  prdsex  13145  prdsvallem  13148  prdsval  13149  prdssca  13151  prdsmulr  13154  imasex  13181  imasival  13182  imasbas  13183  imasplusg  13184  imasmulr  13185  fnmgp  13728  mgpvalg  13729  mgpex  13731  mgpbasg  13732  mgpscag  13733  mgptsetg  13734  mgpdsg  13736  mgpress  13737  ring1  13865  opprvalg  13875  opprex  13879  opprsllem  13880  rmodislmod  14157  sraval  14243  sralemg  14244  srascag  14248  sravscag  14249  sraipg  14250  sraex  14252  zlmval  14433  zlmlemg  14434  zlmmulrg  14437  zlmsca  14438  zlmvscag  14439  znmul  14448  psrval  14472  fnpsr  14473  setsmsdsg  14996  cosz12  15296  sinpi  15301  sinhalfpilem  15307  coshalfpi  15313  sincosq1lem  15341  tangtx  15354  sincos4thpi  15356  tan4thpi  15357  sincos6thpi  15358  sincos3rdpi  15359  pigt3  15360  logltb  15390  lgsdir2lem4  15552  lgsdir2lem5  15553