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  8910  infrenegsupex  9592  xrnegiso  11265  infxrnegsupex  11266  cos01bnd  11761  cos1bnd  11762  cos2bnd  11763  sincos2sgn  11768  sin4lt0  11769  egt2lt3  11782  ssnnctlemct  12441  slotslfn  12482  strslfvd  12498  strslfv2d  12499  strslfv  12501  strsl0  12505  setsslid  12507  setsslnid  12508  rngplusgg  12589  rngmulrg  12590  srngplusgd  12600  srngmulrd  12601  srnginvld  12602  lmodplusgd  12618  lmodscad  12619  lmodvscad  12620  ipsaddgd  12630  ipsmulrd  12631  ipsscad  12632  ipsvscad  12633  ipsipd  12634  topgrpplusgd  12647  topgrptsetd  12648  imasex  12708  imasival  12709  imasbas  12710  imasplusg  12711  imasmulr  12712  fnmgp  13085  mgpvalg  13086  mgpex  13088  mgpbasg  13089  mgpscag  13090  mgptsetg  13091  mgpdsg  13093  mgpress  13094  ring1  13189  opprvalg  13194  opprex  13198  opprsllem  13199  setsmsdsg  13873  cosz12  14094  sinpi  14099  sinhalfpilem  14105  coshalfpi  14111  sincosq1lem  14139  tangtx  14152  sincos4thpi  14154  tan4thpi  14155  sincos6thpi  14156  sincos3rdpi  14157  pigt3  14158  logltb  14188  lgsdir2lem4  14325  lgsdir2lem5  14326