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  4686  eninl  7390  eninr  7391  pw1ne1  7541  negiso  9234  infrenegsupex  9932  xrnegiso  11955  infxrnegsupex  11956  cos01bnd  12452  cos1bnd  12453  cos2bnd  12454  sincos2sgn  12460  sin4lt0  12461  egt2lt3  12474  ssnnctlemct  13218  slotslfn  13259  strslfvd  13275  strslfv2d  13276  strslfv  13278  strslfv3  13279  strsl0  13282  setsslid  13284  setsslnid  13285  rngplusgg  13371  rngmulrg  13372  srngplusgd  13382  srngmulrd  13383  srnginvld  13384  lmodplusgd  13400  lmodscad  13401  lmodvscad  13402  ipsaddgd  13412  ipsmulrd  13413  ipsscad  13414  ipsvscad  13415  ipsipd  13416  topgrpplusgd  13432  topgrptsetd  13433  prdsex  13503  prdsvallem  13506  prdsval  13507  prdssca  13509  prdsmulr  13512  imasex  13539  imasival  13540  imasbas  13541  imasplusg  13542  imasmulr  13543  fnmgp  14087  mgpvalg  14088  mgpex  14090  mgpbasg  14091  mgpscag  14092  mgptsetg  14093  mgpdsg  14095  mgpress  14096  ring1  14224  opprvalg  14234  opprex  14238  opprsllem  14239  rmodislmod  14548  sraval  14634  sralemg  14635  srascag  14639  sravscag  14640  sraipg  14641  sraex  14643  zlmval  14824  zlmlemg  14825  zlmmulrg  14828  zlmsca  14829  zlmvscag  14830  znmul  14839  psrval  14863  fnpsr  14864  setsmsdsg  15394  cosz12  15694  sinpi  15699  sinhalfpilem  15705  coshalfpi  15711  sincosq1lem  15739  tangtx  15752  sincos4thpi  15754  tan4thpi  15755  sincos6thpi  15756  sincos3rdpi  15757  pigt3  15758  logltb  15788  lgsdir2lem4  15953  lgsdir2lem5  15954