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  4658  eninl  7290  eninr  7291  pw1ne1  7440  negiso  9128  infrenegsupex  9821  xrnegiso  11816  infxrnegsupex  11817  cos01bnd  12312  cos1bnd  12313  cos2bnd  12314  sincos2sgn  12320  sin4lt0  12321  egt2lt3  12334  ssnnctlemct  13060  slotslfn  13101  strslfvd  13117  strslfv2d  13118  strslfv  13120  strslfv3  13121  strsl0  13124  setsslid  13126  setsslnid  13127  rngplusgg  13213  rngmulrg  13214  srngplusgd  13224  srngmulrd  13225  srnginvld  13226  lmodplusgd  13242  lmodscad  13243  lmodvscad  13244  ipsaddgd  13254  ipsmulrd  13255  ipsscad  13256  ipsvscad  13257  ipsipd  13258  topgrpplusgd  13274  topgrptsetd  13275  prdsex  13345  prdsvallem  13348  prdsval  13349  prdssca  13351  prdsmulr  13354  imasex  13381  imasival  13382  imasbas  13383  imasplusg  13384  imasmulr  13385  fnmgp  13928  mgpvalg  13929  mgpex  13931  mgpbasg  13932  mgpscag  13933  mgptsetg  13934  mgpdsg  13936  mgpress  13937  ring1  14065  opprvalg  14075  opprex  14079  opprsllem  14080  rmodislmod  14358  sraval  14444  sralemg  14445  srascag  14449  sravscag  14450  sraipg  14451  sraex  14453  zlmval  14634  zlmlemg  14635  zlmmulrg  14638  zlmsca  14639  zlmvscag  14640  znmul  14649  psrval  14673  fnpsr  14674  setsmsdsg  15197  cosz12  15497  sinpi  15502  sinhalfpilem  15508  coshalfpi  15514  sincosq1lem  15542  tangtx  15555  sincos4thpi  15557  tan4thpi  15558  sincos6thpi  15559  sincos3rdpi  15560  pigt3  15561  logltb  15591  lgsdir2lem4  15753  lgsdir2lem5  15754