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  4562  eninl  7096  eninr  7097  pw1ne1  7228  negiso  8912  infrenegsupex  9594  xrnegiso  11270  infxrnegsupex  11271  cos01bnd  11766  cos1bnd  11767  cos2bnd  11768  sincos2sgn  11773  sin4lt0  11774  egt2lt3  11787  ssnnctlemct  12447  slotslfn  12488  strslfvd  12504  strslfv2d  12505  strslfv  12507  strsl0  12511  setsslid  12513  setsslnid  12514  rngplusgg  12595  rngmulrg  12596  srngplusgd  12606  srngmulrd  12607  srnginvld  12608  lmodplusgd  12624  lmodscad  12625  lmodvscad  12626  ipsaddgd  12636  ipsmulrd  12637  ipsscad  12638  ipsvscad  12639  ipsipd  12640  topgrpplusgd  12653  topgrptsetd  12654  prdsex  12718  imasex  12726  imasival  12727  imasbas  12728  imasplusg  12729  imasmulr  12730  fnmgp  13132  mgpvalg  13133  mgpex  13135  mgpbasg  13136  mgpscag  13137  mgptsetg  13138  mgpdsg  13140  mgpress  13141  ring1  13236  opprvalg  13241  opprex  13245  opprsllem  13246  rmodislmod  13441  setsmsdsg  13983  cosz12  14204  sinpi  14209  sinhalfpilem  14215  coshalfpi  14221  sincosq1lem  14249  tangtx  14262  sincos4thpi  14264  tan4thpi  14265  sincos6thpi  14266  sincos3rdpi  14267  pigt3  14268  logltb  14298  lgsdir2lem4  14435  lgsdir2lem5  14436