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  712  mptxor  1435  sb4bor  1846  ordsoexmid  4595  eninl  7158  eninr  7159  pw1ne1  7291  negiso  8976  infrenegsupex  9662  xrnegiso  11408  infxrnegsupex  11409  cos01bnd  11904  cos1bnd  11905  cos2bnd  11906  sincos2sgn  11912  sin4lt0  11913  egt2lt3  11926  ssnnctlemct  12606  slotslfn  12647  strslfvd  12663  strslfv2d  12664  strslfv  12666  strsl0  12670  setsslid  12672  setsslnid  12673  rngplusgg  12757  rngmulrg  12758  srngplusgd  12768  srngmulrd  12769  srnginvld  12770  lmodplusgd  12786  lmodscad  12787  lmodvscad  12788  ipsaddgd  12798  ipsmulrd  12799  ipsscad  12800  ipsvscad  12801  ipsipd  12802  topgrpplusgd  12818  topgrptsetd  12819  prdsex  12883  imasex  12891  imasival  12892  imasbas  12893  imasplusg  12894  imasmulr  12895  fnmgp  13421  mgpvalg  13422  mgpex  13424  mgpbasg  13425  mgpscag  13426  mgptsetg  13427  mgpdsg  13429  mgpress  13430  ring1  13558  opprvalg  13568  opprex  13572  opprsllem  13573  rmodislmod  13850  sraval  13936  sralemg  13937  srascag  13941  sravscag  13942  sraipg  13943  sraex  13945  zlmval  14126  zlmlemg  14127  zlmmulrg  14130  zlmsca  14131  zlmvscag  14132  znmul  14141  psrval  14163  fnpsr  14164  setsmsdsg  14659  cosz12  14956  sinpi  14961  sinhalfpilem  14967  coshalfpi  14973  sincosq1lem  15001  tangtx  15014  sincos4thpi  15016  tan4thpi  15017  sincos6thpi  15018  sincos3rdpi  15019  pigt3  15020  logltb  15050  lgsdir2lem4  15188  lgsdir2lem5  15189