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 ⊢ 𝜓

This proof depends on syntax axioms:   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-ia2 107

This theorem is used by:  bi3  119  dfbi2  392  olc  723  mptxor  1473  sb4bor  1888  ordsoexmid  4709  eninl  7438  eninr  7439  pw1ne1  7589  negiso  9288  infrenegsupex  10004  xrnegiso  12046  infxrnegsupex  12047  cos01bnd  12543  cos1bnd  12544  cos2bnd  12545  sincos2sgn  12551  sin4lt0  12552  egt2lt3  12565  ssnnctlemct  13388  slotslfn  13429  strslfvd  13445  strslfv2d  13446  strslfv  13448  strslfv3  13449  strsl0  13452  setsslid  13454  setsslnid  13455  slotm  13466  rngplusgg  13542  rngmulrg  13543  srngplusgd  13553  srngmulrd  13554  srnginvld  13555  lmodplusgd  13571  lmodscad  13572  lmodvscad  13573  ipsaddgd  13583  ipsmulrd  13584  ipsscad  13585  ipsvscad  13586  ipsipd  13587  topgrpplusgd  13603  topgrptsetd  13604  prdsvallem  13672  imasex  13677  imasival  13678  imasbas  13679  imasplusg  13680  imasmulr  13681  prdsex  14223  prdsval  14224  prdssca  14226  prdsmulr  14229  fnmgp  14270  mgpvalg  14271  mgpex  14274  mgpbasg  14275  mgpscag  14277  mgptsetg  14278  mgpdsg  14280  mgpress  14281  ring1  14415  opprvalg  14425  opprex  14429  opprsllem  14430  rmodislmod  14739  sraval  14825  sralemg  14826  srascag  14830  sravscag  14831  sraipg  14832  sraex  14834  zlmval  15013  zlmlemg  15014  zlmmulrg  15017  zlmsca  15018  zlmvscag  15019  znmul  15028  psrval  15101  fnpsr  15102  setsmsdsg  15633  cosz12  15934  sinpi  15939  sinhalfpilem  15945  coshalfpi  15951  sincosq1lem  15979  tangtx  15992  sincos4thpi  15994  tan4thpi  15995  sincos6thpi  15996  sincos3rdpi  15997  pigt3  15998  logltb  16029  log2tlbndlog2  16142  ppiublem1  16213  ppiublem2  16214  lgsdir2lem4  16272  lgsdir2lem5  16273