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

Syntax hints:   ∧ wa 104

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

This theorem is referenced by:  bi3  119  dfbi2  388  olc  718  mptxor  1468  sb4bor  1882  ordsoexmid  4662  eninl  7301  eninr  7302  pw1ne1  7452  negiso  9140  infrenegsupex  9833  xrnegiso  11845  infxrnegsupex  11846  cos01bnd  12342  cos1bnd  12343  cos2bnd  12344  sincos2sgn  12350  sin4lt0  12351  egt2lt3  12364  ssnnctlemct  13090  slotslfn  13131  strslfvd  13147  strslfv2d  13148  strslfv  13150  strslfv3  13151  strsl0  13154  setsslid  13156  setsslnid  13157  rngplusgg  13243  rngmulrg  13244  srngplusgd  13254  srngmulrd  13255  srnginvld  13256  lmodplusgd  13272  lmodscad  13273  lmodvscad  13274  ipsaddgd  13284  ipsmulrd  13285  ipsscad  13286  ipsvscad  13287  ipsipd  13288  topgrpplusgd  13304  topgrptsetd  13305  prdsex  13375  prdsvallem  13378  prdsval  13379  prdssca  13381  prdsmulr  13384  imasex  13411  imasival  13412  imasbas  13413  imasplusg  13414  imasmulr  13415  fnmgp  13959  mgpvalg  13960  mgpex  13962  mgpbasg  13963  mgpscag  13964  mgptsetg  13965  mgpdsg  13967  mgpress  13968  ring1  14096  opprvalg  14106  opprex  14110  opprsllem  14111  rmodislmod  14389  sraval  14475  sralemg  14476  srascag  14480  sravscag  14481  sraipg  14482  sraex  14484  zlmval  14665  zlmlemg  14666  zlmmulrg  14669  zlmsca  14670  zlmvscag  14671  znmul  14680  psrval  14704  fnpsr  14705  setsmsdsg  15233  cosz12  15533  sinpi  15538  sinhalfpilem  15544  coshalfpi  15550  sincosq1lem  15578  tangtx  15591  sincos4thpi  15593  tan4thpi  15594  sincos6thpi  15595  sincos3rdpi  15596  pigt3  15597  logltb  15627  lgsdir2lem4  15789  lgsdir2lem5  15790