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  716  mptxor  1466  sb4bor  1881  ordsoexmid  4654  eninl  7272  eninr  7273  pw1ne1  7422  negiso  9110  infrenegsupex  9797  xrnegiso  11781  infxrnegsupex  11782  cos01bnd  12277  cos1bnd  12278  cos2bnd  12279  sincos2sgn  12285  sin4lt0  12286  egt2lt3  12299  ssnnctlemct  13025  slotslfn  13066  strslfvd  13082  strslfv2d  13083  strslfv  13085  strslfv3  13086  strsl0  13089  setsslid  13091  setsslnid  13092  rngplusgg  13178  rngmulrg  13179  srngplusgd  13189  srngmulrd  13190  srnginvld  13191  lmodplusgd  13207  lmodscad  13208  lmodvscad  13209  ipsaddgd  13219  ipsmulrd  13220  ipsscad  13221  ipsvscad  13222  ipsipd  13223  topgrpplusgd  13239  topgrptsetd  13240  prdsex  13310  prdsvallem  13313  prdsval  13314  prdssca  13316  prdsmulr  13319  imasex  13346  imasival  13347  imasbas  13348  imasplusg  13349  imasmulr  13350  fnmgp  13893  mgpvalg  13894  mgpex  13896  mgpbasg  13897  mgpscag  13898  mgptsetg  13899  mgpdsg  13901  mgpress  13902  ring1  14030  opprvalg  14040  opprex  14044  opprsllem  14045  rmodislmod  14323  sraval  14409  sralemg  14410  srascag  14414  sravscag  14415  sraipg  14416  sraex  14418  zlmval  14599  zlmlemg  14600  zlmmulrg  14603  zlmsca  14604  zlmvscag  14605  znmul  14614  psrval  14638  fnpsr  14639  setsmsdsg  15162  cosz12  15462  sinpi  15467  sinhalfpilem  15473  coshalfpi  15479  sincosq1lem  15507  tangtx  15520  sincos4thpi  15522  tan4thpi  15523  sincos6thpi  15524  sincos3rdpi  15525  pigt3  15526  logltb  15556  lgsdir2lem4  15718  lgsdir2lem5  15719