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  386  olc  701  mptxor  1414  sb4bor  1823  ordsoexmid  4539  eninl  7062  eninr  7063  pw1ne1  7185  negiso  8850  infrenegsupex  9532  xrnegiso  11203  infxrnegsupex  11204  cos01bnd  11699  cos1bnd  11700  cos2bnd  11701  sincos2sgn  11706  sin4lt0  11707  egt2lt3  11720  ssnnctlemct  12379  slotslfn  12420  strslfvd  12435  strslfv2d  12436  strslfv  12438  strsl0  12442  setsslid  12444  setsslnid  12445  rngplusgg  12512  rngmulrg  12513  srngplusgd  12519  srngmulrd  12520  srnginvld  12521  lmodplusgd  12530  lmodscad  12531  lmodvscad  12532  ipsaddgd  12538  ipsmulrd  12539  ipsscad  12540  ipsvscad  12541  ipsipd  12542  topgrpplusgd  12548  topgrptsetd  12549  setsmsdsg  13130  cosz12  13351  sinpi  13356  sinhalfpilem  13362  coshalfpi  13368  sincosq1lem  13396  tangtx  13409  sincos4thpi  13411  tan4thpi  13412  sincos6thpi  13413  sincos3rdpi  13414  pigt3  13415  logltb  13445  lgsdir2lem4  13582  lgsdir2lem5  13583