Theorem simpri 112

Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)

Hypothesis

Ref	Expression
simpri.1	|- ( ph /\ ps )

Assertion

Ref	Expression
simpri	|- ps

Proof of Theorem simpri

Step	Hyp	Ref	Expression
1		simpri.1	. 2 |- ( ph /\ ps )
2		simpr 109	. 2 |- ( ( ph /\ ps ) -> ps )
3	1, 2	ax-mp 5	1 |- ps

Syntax hints:   /\ wa 103

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

This theorem is referenced by:  bi3  118  dfbi2  385  olc  700  mptxor  1402  sb4bor  1807  ordsoexmid  4477  eninl  6982  eninr  6983  negiso  8713  infrenegsupex  9389  xrnegiso  11031  infxrnegsupex  11032  cos01bnd  11465  cos1bnd  11466  cos2bnd  11467  sincos2sgn  11472  sin4lt0  11473  egt2lt3  11486  slotslfn  11985  strslfvd  12000  strslfv2d  12001  strslfv  12003  strsl0  12007  setsslid  12009  setsslnid  12010  rngplusgg  12076  rngmulrg  12077  srngplusgd  12083  srngmulrd  12084  srnginvld  12085  lmodplusgd  12094  lmodscad  12095  lmodvscad  12096  ipsaddgd  12102  ipsmulrd  12103  ipsscad  12104  ipsvscad  12105  ipsipd  12106  topgrpplusgd  12112  topgrptsetd  12113  setsmsdsg  12649  cosz12  12861  sinpi  12866  sinhalfpilem  12872  coshalfpi  12878  sincosq1lem  12906  tangtx  12919  sincos4thpi  12921  tan4thpi  12922  sincos6thpi  12923  sincos3rdpi  12924  pigt3  12925