Theorem simpri 113

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 110	. 2 |- ( ( ph /\ ps ) -> ps )
3	1, 2	ax-mp 5	1 |- ps

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  711  mptxor  1424  sb4bor  1835  ordsoexmid  4561  eninl  7095  eninr  7096  pw1ne1  7227  negiso  8911  infrenegsupex  9593  xrnegiso  11269  infxrnegsupex  11270  cos01bnd  11765  cos1bnd  11766  cos2bnd  11767  sincos2sgn  11772  sin4lt0  11773  egt2lt3  11786  ssnnctlemct  12446  slotslfn  12487  strslfvd  12503  strslfv2d  12504  strslfv  12506  strsl0  12510  setsslid  12512  setsslnid  12513  rngplusgg  12594  rngmulrg  12595  srngplusgd  12605  srngmulrd  12606  srnginvld  12607  lmodplusgd  12623  lmodscad  12624  lmodvscad  12625  ipsaddgd  12635  ipsmulrd  12636  ipsscad  12637  ipsvscad  12638  ipsipd  12639  topgrpplusgd  12652  topgrptsetd  12653  prdsex  12717  imasex  12725  imasival  12726  imasbas  12727  imasplusg  12728  imasmulr  12729  fnmgp  13130  mgpvalg  13131  mgpex  13133  mgpbasg  13134  mgpscag  13135  mgptsetg  13136  mgpdsg  13138  mgpress  13139  ring1  13234  opprvalg  13239  opprex  13243  opprsllem  13244  setsmsdsg  13950  cosz12  14171  sinpi  14176  sinhalfpilem  14182  coshalfpi  14188  sincosq1lem  14216  tangtx  14229  sincos4thpi  14231  tan4thpi  14232  sincos6thpi  14233  sincos3rdpi  14234  pigt3  14235  logltb  14265  lgsdir2lem4  14402  lgsdir2lem5  14403