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  718  mptxor  1468  sb4bor  1883  ordsoexmid  4660  eninl  7296  eninr  7297  pw1ne1  7447  negiso  9135  infrenegsupex  9828  xrnegiso  11840  infxrnegsupex  11841  cos01bnd  12337  cos1bnd  12338  cos2bnd  12339  sincos2sgn  12345  sin4lt0  12346  egt2lt3  12359  ssnnctlemct  13085  slotslfn  13126  strslfvd  13142  strslfv2d  13143  strslfv  13145  strslfv3  13146  strsl0  13149  setsslid  13151  setsslnid  13152  rngplusgg  13238  rngmulrg  13239  srngplusgd  13249  srngmulrd  13250  srnginvld  13251  lmodplusgd  13267  lmodscad  13268  lmodvscad  13269  ipsaddgd  13279  ipsmulrd  13280  ipsscad  13281  ipsvscad  13282  ipsipd  13283  topgrpplusgd  13299  topgrptsetd  13300  prdsex  13370  prdsvallem  13373  prdsval  13374  prdssca  13376  prdsmulr  13379  imasex  13406  imasival  13407  imasbas  13408  imasplusg  13409  imasmulr  13410  fnmgp  13954  mgpvalg  13955  mgpex  13957  mgpbasg  13958  mgpscag  13959  mgptsetg  13960  mgpdsg  13962  mgpress  13963  ring1  14091  opprvalg  14101  opprex  14105  opprsllem  14106  rmodislmod  14384  sraval  14470  sralemg  14471  srascag  14475  sravscag  14476  sraipg  14477  sraex  14479  zlmval  14660  zlmlemg  14661  zlmmulrg  14664  zlmsca  14665  zlmvscag  14666  znmul  14675  psrval  14699  fnpsr  14700  setsmsdsg  15223  cosz12  15523  sinpi  15528  sinhalfpilem  15534  coshalfpi  15540  sincosq1lem  15568  tangtx  15581  sincos4thpi  15583  tan4thpi  15584  sincos6thpi  15585  sincos3rdpi  15586  pigt3  15587  logltb  15617  lgsdir2lem4  15779  lgsdir2lem5  15780