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  7437  eninr  7438  pw1ne1  7588  negiso  9286  infrenegsupex  9996  xrnegiso  12030  infxrnegsupex  12031  cos01bnd  12527  cos1bnd  12528  cos2bnd  12529  sincos2sgn  12535  sin4lt0  12536  egt2lt3  12549  ssnnctlemct  13339  slotslfn  13380  strslfvd  13396  strslfv2d  13397  strslfv  13399  strslfv3  13400  strsl0  13403  setsslid  13405  setsslnid  13406  slotm  13417  rngplusgg  13493  rngmulrg  13494  srngplusgd  13504  srngmulrd  13505  srnginvld  13506  lmodplusgd  13522  lmodscad  13523  lmodvscad  13524  ipsaddgd  13534  ipsmulrd  13535  ipsscad  13536  ipsvscad  13537  ipsipd  13538  topgrpplusgd  13554  topgrptsetd  13555  prdsvallem  13623  imasex  13628  imasival  13629  imasbas  13630  imasplusg  13631  imasmulr  13632  prdsex  14174  prdsval  14175  prdssca  14177  prdsmulr  14180  fnmgp  14221  mgpvalg  14222  mgpex  14225  mgpbasg  14226  mgpscag  14228  mgptsetg  14229  mgpdsg  14231  mgpress  14232  ring1  14366  opprvalg  14376  opprex  14380  opprsllem  14381  rmodislmod  14690  sraval  14776  sralemg  14777  srascag  14781  sravscag  14782  sraipg  14783  sraex  14785  zlmval  14964  zlmlemg  14965  zlmmulrg  14968  zlmsca  14969  zlmvscag  14970  znmul  14979  psrval  15052  fnpsr  15053  setsmsdsg  15583  cosz12  15884  sinpi  15889  sinhalfpilem  15895  coshalfpi  15901  sincosq1lem  15929  tangtx  15942  sincos4thpi  15944  tan4thpi  15945  sincos6thpi  15946  sincos3rdpi  15947  pigt3  15948  logltb  15979  log2tlbndlog2  16088  lgsdir2lem4  16162  lgsdir2lem5  16163