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  386  olc  701  mptxor  1414  sb4bor  1823  ordsoexmid  4539  eninl  7062  eninr  7063  pw1ne1  7185  negiso  8850  infrenegsupex  9532  xrnegiso  11203  infxrnegsupex  11204  cos01bnd  11699  cos1bnd  11700  cos2bnd  11701  sincos2sgn  11706  sin4lt0  11707  egt2lt3  11720  ssnnctlemct  12379  slotslfn  12420  strslfvd  12435  strslfv2d  12436  strslfv  12438  strsl0  12442  setsslid  12444  setsslnid  12445  rngplusgg  12512  rngmulrg  12513  srngplusgd  12519  srngmulrd  12520  srnginvld  12521  lmodplusgd  12530  lmodscad  12531  lmodvscad  12532  ipsaddgd  12538  ipsmulrd  12539  ipsscad  12540  ipsvscad  12541  ipsipd  12542  topgrpplusgd  12548  topgrptsetd  12549  setsmsdsg  13120  cosz12  13341  sinpi  13346  sinhalfpilem  13352  coshalfpi  13358  sincosq1lem  13386  tangtx  13399  sincos4thpi  13401  tan4thpi  13402  sincos6thpi  13403  sincos3rdpi  13404  pigt3  13405  logltb  13435  lgsdir2lem4  13572  lgsdir2lem5  13573