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  4617  eninl  7213  eninr  7214  pw1ne1  7356  negiso  9043  infrenegsupex  9730  xrnegiso  11643  infxrnegsupex  11644  cos01bnd  12139  cos1bnd  12140  cos2bnd  12141  sincos2sgn  12147  sin4lt0  12148  egt2lt3  12161  ssnnctlemct  12887  slotslfn  12928  strslfvd  12944  strslfv2d  12945  strslfv  12947  strslfv3  12948  strsl0  12951  setsslid  12953  setsslnid  12954  rngplusgg  13039  rngmulrg  13040  srngplusgd  13050  srngmulrd  13051  srnginvld  13052  lmodplusgd  13068  lmodscad  13069  lmodvscad  13070  ipsaddgd  13080  ipsmulrd  13081  ipsscad  13082  ipsvscad  13083  ipsipd  13084  topgrpplusgd  13100  topgrptsetd  13101  prdsex  13171  prdsvallem  13174  prdsval  13175  prdssca  13177  prdsmulr  13180  imasex  13207  imasival  13208  imasbas  13209  imasplusg  13210  imasmulr  13211  fnmgp  13754  mgpvalg  13755  mgpex  13757  mgpbasg  13758  mgpscag  13759  mgptsetg  13760  mgpdsg  13762  mgpress  13763  ring1  13891  opprvalg  13901  opprex  13905  opprsllem  13906  rmodislmod  14183  sraval  14269  sralemg  14270  srascag  14274  sravscag  14275  sraipg  14276  sraex  14278  zlmval  14459  zlmlemg  14460  zlmmulrg  14463  zlmsca  14464  zlmvscag  14465  znmul  14474  psrval  14498  fnpsr  14499  setsmsdsg  15022  cosz12  15322  sinpi  15327  sinhalfpilem  15333  coshalfpi  15339  sincosq1lem  15367  tangtx  15380  sincos4thpi  15382  tan4thpi  15383  sincos6thpi  15384  sincos3rdpi  15385  pigt3  15386  logltb  15416  lgsdir2lem4  15578  lgsdir2lem5  15579