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  1883  ordsoexmid  4660  eninl  7296  eninr  7297  pw1ne1  7447  negiso  9135  infrenegsupex  9828  xrnegiso  11824  infxrnegsupex  11825  cos01bnd  12321  cos1bnd  12322  cos2bnd  12323  sincos2sgn  12329  sin4lt0  12330  egt2lt3  12343  ssnnctlemct  13069  slotslfn  13110  strslfvd  13126  strslfv2d  13127  strslfv  13129  strslfv3  13130  strsl0  13133  setsslid  13135  setsslnid  13136  rngplusgg  13222  rngmulrg  13223  srngplusgd  13233  srngmulrd  13234  srnginvld  13235  lmodplusgd  13251  lmodscad  13252  lmodvscad  13253  ipsaddgd  13263  ipsmulrd  13264  ipsscad  13265  ipsvscad  13266  ipsipd  13267  topgrpplusgd  13283  topgrptsetd  13284  prdsex  13354  prdsvallem  13357  prdsval  13358  prdssca  13360  prdsmulr  13363  imasex  13390  imasival  13391  imasbas  13392  imasplusg  13393  imasmulr  13394  fnmgp  13938  mgpvalg  13939  mgpex  13941  mgpbasg  13942  mgpscag  13943  mgptsetg  13944  mgpdsg  13946  mgpress  13947  ring1  14075  opprvalg  14085  opprex  14089  opprsllem  14090  rmodislmod  14368  sraval  14454  sralemg  14455  srascag  14459  sravscag  14460  sraipg  14461  sraex  14463  zlmval  14644  zlmlemg  14645  zlmmulrg  14648  zlmsca  14649  zlmvscag  14650  znmul  14659  psrval  14683  fnpsr  14684  setsmsdsg  15207  cosz12  15507  sinpi  15512  sinhalfpilem  15518  coshalfpi  15524  sincosq1lem  15552  tangtx  15565  sincos4thpi  15567  tan4thpi  15568  sincos6thpi  15569  sincos3rdpi  15570  pigt3  15571  logltb  15601  lgsdir2lem4  15763  lgsdir2lem5  15764