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  716  mptxor  1466  sb4bor  1881  ordsoexmid  4655  eninl  7280  eninr  7281  pw1ne1  7430  negiso  9118  infrenegsupex  9806  xrnegiso  11794  infxrnegsupex  11795  cos01bnd  12290  cos1bnd  12291  cos2bnd  12292  sincos2sgn  12298  sin4lt0  12299  egt2lt3  12312  ssnnctlemct  13038  slotslfn  13079  strslfvd  13095  strslfv2d  13096  strslfv  13098  strslfv3  13099  strsl0  13102  setsslid  13104  setsslnid  13105  rngplusgg  13191  rngmulrg  13192  srngplusgd  13202  srngmulrd  13203  srnginvld  13204  lmodplusgd  13220  lmodscad  13221  lmodvscad  13222  ipsaddgd  13232  ipsmulrd  13233  ipsscad  13234  ipsvscad  13235  ipsipd  13236  topgrpplusgd  13252  topgrptsetd  13253  prdsex  13323  prdsvallem  13326  prdsval  13327  prdssca  13329  prdsmulr  13332  imasex  13359  imasival  13360  imasbas  13361  imasplusg  13362  imasmulr  13363  fnmgp  13906  mgpvalg  13907  mgpex  13909  mgpbasg  13910  mgpscag  13911  mgptsetg  13912  mgpdsg  13914  mgpress  13915  ring1  14043  opprvalg  14053  opprex  14057  opprsllem  14058  rmodislmod  14336  sraval  14422  sralemg  14423  srascag  14427  sravscag  14428  sraipg  14429  sraex  14431  zlmval  14612  zlmlemg  14613  zlmmulrg  14616  zlmsca  14617  zlmvscag  14618  znmul  14627  psrval  14651  fnpsr  14652  setsmsdsg  15175  cosz12  15475  sinpi  15480  sinhalfpilem  15486  coshalfpi  15492  sincosq1lem  15520  tangtx  15533  sincos4thpi  15535  tan4thpi  15536  sincos6thpi  15537  sincos3rdpi  15538  pigt3  15539  logltb  15569  lgsdir2lem4  15731  lgsdir2lem5  15732