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 7	1 |- ps

Syntax hints:   /\ wa 103

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

This theorem is referenced by:  bi3  118  dfbi2  383  olc  683  mptxor  1383  sb4bor  1787  ordsoexmid  4435  eninl  6932  eninr  6933  negiso  8617  infrenegsupex  9285  xrnegiso  10917  infxrnegsupex  10918  cos01bnd  11310  cos1bnd  11311  cos2bnd  11312  sincos2sgn  11317  sin4lt0  11318  egt2lt3  11328  slotslfn  11822  strslfvd  11837  strslfv2d  11838  strslfv  11840  strsl0  11844  setsslid  11846  setsslnid  11847  rngplusgg  11913  rngmulrg  11914  srngplusgd  11920  srngmulrd  11921  srnginvld  11922  lmodplusgd  11931  lmodscad  11932  lmodvscad  11933  ipsaddgd  11939  ipsmulrd  11940  ipsscad  11941  ipsvscad  11942  ipsipd  11943  topgrpplusgd  11949  topgrptsetd  11950  setsmsdsg  12463