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  706  mptxor  1419  sb4bor  1828  ordsoexmid  4546  eninl  7074  eninr  7075  pw1ne1  7206  negiso  8871  infrenegsupex  9553  xrnegiso  11225  infxrnegsupex  11226  cos01bnd  11721  cos1bnd  11722  cos2bnd  11723  sincos2sgn  11728  sin4lt0  11729  egt2lt3  11742  ssnnctlemct  12401  slotslfn  12442  strslfvd  12457  strslfv2d  12458  strslfv  12460  strsl0  12464  setsslid  12466  setsslnid  12467  rngplusgg  12535  rngmulrg  12536  srngplusgd  12542  srngmulrd  12543  srnginvld  12544  lmodplusgd  12553  lmodscad  12554  lmodvscad  12555  ipsaddgd  12561  ipsmulrd  12562  ipsscad  12563  ipsvscad  12564  ipsipd  12565  topgrpplusgd  12571  topgrptsetd  12572  setsmsdsg  13274  cosz12  13495  sinpi  13500  sinhalfpilem  13506  coshalfpi  13512  sincosq1lem  13540  tangtx  13553  sincos4thpi  13555  tan4thpi  13556  sincos6thpi  13557  sincos3rdpi  13558  pigt3  13559  logltb  13589  lgsdir2lem4  13726  lgsdir2lem5  13727