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  712  mptxor  1435  sb4bor  1849  ordsoexmid  4599  eninl  7172  eninr  7173  pw1ne1  7312  negiso  8999  infrenegsupex  9685  xrnegiso  11444  infxrnegsupex  11445  cos01bnd  11940  cos1bnd  11941  cos2bnd  11942  sincos2sgn  11948  sin4lt0  11949  egt2lt3  11962  ssnnctlemct  12688  slotslfn  12729  strslfvd  12745  strslfv2d  12746  strslfv  12748  strslfv3  12749  strsl0  12752  setsslid  12754  setsslnid  12755  rngplusgg  12839  rngmulrg  12840  srngplusgd  12850  srngmulrd  12851  srnginvld  12852  lmodplusgd  12868  lmodscad  12869  lmodvscad  12870  ipsaddgd  12880  ipsmulrd  12881  ipsscad  12882  ipsvscad  12883  ipsipd  12884  topgrpplusgd  12900  topgrptsetd  12901  prdsex  12971  prdsvallem  12974  prdsval  12975  prdssca  12977  prdsmulr  12980  imasex  13007  imasival  13008  imasbas  13009  imasplusg  13010  imasmulr  13011  fnmgp  13554  mgpvalg  13555  mgpex  13557  mgpbasg  13558  mgpscag  13559  mgptsetg  13560  mgpdsg  13562  mgpress  13563  ring1  13691  opprvalg  13701  opprex  13705  opprsllem  13706  rmodislmod  13983  sraval  14069  sralemg  14070  srascag  14074  sravscag  14075  sraipg  14076  sraex  14078  zlmval  14259  zlmlemg  14260  zlmmulrg  14263  zlmsca  14264  zlmvscag  14265  znmul  14274  psrval  14296  fnpsr  14297  setsmsdsg  14800  cosz12  15100  sinpi  15105  sinhalfpilem  15111  coshalfpi  15117  sincosq1lem  15145  tangtx  15158  sincos4thpi  15160  tan4thpi  15161  sincos6thpi  15162  sincos3rdpi  15163  pigt3  15164  logltb  15194  lgsdir2lem4  15356  lgsdir2lem5  15357