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  4594  eninl  7156  eninr  7157  pw1ne1  7289  negiso  8974  infrenegsupex  9659  xrnegiso  11405  infxrnegsupex  11406  cos01bnd  11901  cos1bnd  11902  cos2bnd  11903  sincos2sgn  11909  sin4lt0  11910  egt2lt3  11923  ssnnctlemct  12603  slotslfn  12644  strslfvd  12660  strslfv2d  12661  strslfv  12663  strsl0  12667  setsslid  12669  setsslnid  12670  rngplusgg  12754  rngmulrg  12755  srngplusgd  12765  srngmulrd  12766  srnginvld  12767  lmodplusgd  12783  lmodscad  12784  lmodvscad  12785  ipsaddgd  12795  ipsmulrd  12796  ipsscad  12797  ipsvscad  12798  ipsipd  12799  topgrpplusgd  12815  topgrptsetd  12816  prdsex  12880  imasex  12888  imasival  12889  imasbas  12890  imasplusg  12891  imasmulr  12892  fnmgp  13418  mgpvalg  13419  mgpex  13421  mgpbasg  13422  mgpscag  13423  mgptsetg  13424  mgpdsg  13426  mgpress  13427  ring1  13555  opprvalg  13565  opprex  13569  opprsllem  13570  rmodislmod  13847  sraval  13933  sralemg  13934  srascag  13938  sravscag  13939  sraipg  13940  sraex  13942  zlmval  14115  zlmlemg  14116  zlmmulrg  14119  zlmsca  14120  zlmvscag  14121  znmul  14130  psrval  14152  fnpsr  14153  setsmsdsg  14648  cosz12  14915  sinpi  14920  sinhalfpilem  14926  coshalfpi  14932  sincosq1lem  14960  tangtx  14973  sincos4thpi  14975  tan4thpi  14976  sincos6thpi  14977  sincos3rdpi  14978  pigt3  14979  logltb  15009  lgsdir2lem4  15147  lgsdir2lem5  15148