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  4711  eninl  7444  eninr  7445  pw1ne1  7595  negiso  9294  infrenegsupex  10011  xrnegiso  12054  infxrnegsupex  12055  cos01bnd  12551  cos1bnd  12552  cos2bnd  12553  sincos2sgn  12559  sin4lt0  12560  egt2lt3  12573  ssnnctlemct  13396  slotslfn  13437  strslfvd  13453  strslfv2d  13454  strslfv  13456  strslfv3  13457  strsl0  13460  setsslid  13462  setsslnid  13463  slotm  13474  rngplusgg  13551  rngmulrg  13552  srngplusgd  13562  srngmulrd  13563  srnginvld  13564  lmodplusgd  13580  lmodscad  13581  lmodvscad  13582  ipsaddgd  13592  ipsmulrd  13593  ipsscad  13594  ipsvscad  13595  ipsipd  13596  topgrpplusgd  13612  topgrptsetd  13613  prdsvallem  13681  imasex  13686  imasival  13687  imasbas  13688  imasplusg  13689  imasmulr  13690  prdsex  14280  prdsval  14281  prdssca  14283  prdsmulr  14286  fnmgp  14327  mgpvalg  14328  mgpex  14331  mgpbasg  14332  mgpscag  14334  mgptsetg  14335  mgpdsg  14337  mgpress  14338  ring1  14472  opprvalg  14484  opprex  14488  opprsllem  14489  rmodislmod  14798  sraval  14884  sralemg  14885  srascag  14889  sravscag  14890  sraipg  14891  sraex  14893  zlmval  15072  zlmlemg  15073  zlmmulrg  15076  zlmsca  15077  zlmvscag  15078  znmul  15087  psrval  15162  fnpsr  15163  setsmsdsg  15718  cosz12  16019  sinpi  16024  sinhalfpilem  16030  coshalfpi  16036  sincosq1lem  16064  tangtx  16077  sincos4thpi  16079  tan4thpi  16080  sincos6thpi  16081  sincos3rdpi  16082  pigt3  16083  logltb  16116  log2tlbndlog2  16232  ppiublem1  16303  ppiublem2  16304  bposlem9  16331  lgsdir2lem4  16367  lgsdir2lem5  16368