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  719  mptxor  1469  sb4bor  1884  ordsoexmid  4683  eninl  7387  eninr  7388  pw1ne1  7538  negiso  9225  infrenegsupex  9922  xrnegiso  11940  infxrnegsupex  11941  cos01bnd  12437  cos1bnd  12438  cos2bnd  12439  sincos2sgn  12445  sin4lt0  12446  egt2lt3  12459  ssnnctlemct  13186  slotslfn  13227  strslfvd  13243  strslfv2d  13244  strslfv  13246  strslfv3  13247  strsl0  13250  setsslid  13252  setsslnid  13253  rngplusgg  13339  rngmulrg  13340  srngplusgd  13350  srngmulrd  13351  srnginvld  13352  lmodplusgd  13368  lmodscad  13369  lmodvscad  13370  ipsaddgd  13380  ipsmulrd  13381  ipsscad  13382  ipsvscad  13383  ipsipd  13384  topgrpplusgd  13400  topgrptsetd  13401  prdsex  13471  prdsvallem  13474  prdsval  13475  prdssca  13477  prdsmulr  13480  imasex  13507  imasival  13508  imasbas  13509  imasplusg  13510  imasmulr  13511  fnmgp  14055  mgpvalg  14056  mgpex  14058  mgpbasg  14059  mgpscag  14060  mgptsetg  14061  mgpdsg  14063  mgpress  14064  ring1  14192  opprvalg  14202  opprex  14206  opprsllem  14207  rmodislmod  14486  sraval  14572  sralemg  14573  srascag  14577  sravscag  14578  sraipg  14579  sraex  14581  zlmval  14762  zlmlemg  14763  zlmmulrg  14766  zlmsca  14767  zlmvscag  14768  znmul  14777  psrval  14801  fnpsr  14802  setsmsdsg  15332  cosz12  15632  sinpi  15637  sinhalfpilem  15643  coshalfpi  15649  sincosq1lem  15677  tangtx  15690  sincos4thpi  15692  tan4thpi  15693  sincos6thpi  15694  sincos3rdpi  15695  pigt3  15696  logltb  15726  lgsdir2lem4  15891  lgsdir2lem5  15892