Theorem simpri 112

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 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3	1, 2	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-ia2 106

This theorem is referenced by:  bi3  118  dfbi2  385  olc  700  mptxor  1402  sb4bor  1807  ordsoexmid  4477  eninl  6982  eninr  6983  negiso  8716  infrenegsupex  9392  xrnegiso  11034  infxrnegsupex  11035  cos01bnd  11468  cos1bnd  11469  cos2bnd  11470  sincos2sgn  11475  sin4lt0  11476  egt2lt3  11489  slotslfn  11988  strslfvd  12003  strslfv2d  12004  strslfv  12006  strsl0  12010  setsslid  12012  setsslnid  12013  rngplusgg  12079  rngmulrg  12080  srngplusgd  12086  srngmulrd  12087  srnginvld  12088  lmodplusgd  12097  lmodscad  12098  lmodvscad  12099  ipsaddgd  12105  ipsmulrd  12106  ipsscad  12107  ipsvscad  12108  ipsipd  12109  topgrpplusgd  12115  topgrptsetd  12116  setsmsdsg  12652  cosz12  12864  sinpi  12869  sinhalfpilem  12875  coshalfpi  12881  sincosq1lem  12909  tangtx  12922  sincos4thpi  12924  tan4thpi  12925  sincos6thpi  12926  sincos3rdpi  12927  pigt3  12928