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

This proof depends on syntax axioms:   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-ia2 107

This theorem is used by:  bi3  119  dfbi2  392  olc  723  mptxor  1473  sb4bor  1888  ordsoexmid  4709  eninl  7437  eninr  7438  pw1ne1  7588  negiso  9287  infrenegsupex  10003  xrnegiso  12044  infxrnegsupex  12045  cos01bnd  12541  cos1bnd  12542  cos2bnd  12543  sincos2sgn  12549  sin4lt0  12550  egt2lt3  12563  ssnnctlemct  13386  slotslfn  13427  strslfvd  13443  strslfv2d  13444  strslfv  13446  strslfv3  13447  strsl0  13450  setsslid  13452  setsslnid  13453  slotm  13464  rngplusgg  13540  rngmulrg  13541  srngplusgd  13551  srngmulrd  13552  srnginvld  13553  lmodplusgd  13569  lmodscad  13570  lmodvscad  13571  ipsaddgd  13581  ipsmulrd  13582  ipsscad  13583  ipsvscad  13584  ipsipd  13585  topgrpplusgd  13601  topgrptsetd  13602  prdsvallem  13670  imasex  13675  imasival  13676  imasbas  13677  imasplusg  13678  imasmulr  13679  prdsex  14221  prdsval  14222  prdssca  14224  prdsmulr  14227  fnmgp  14268  mgpvalg  14269  mgpex  14272  mgpbasg  14273  mgpscag  14275  mgptsetg  14276  mgpdsg  14278  mgpress  14279  ring1  14413  opprvalg  14423  opprex  14427  opprsllem  14428  rmodislmod  14737  sraval  14823  sralemg  14824  srascag  14828  sravscag  14829  sraipg  14830  sraex  14832  zlmval  15011  zlmlemg  15012  zlmmulrg  15015  zlmsca  15016  zlmvscag  15017  znmul  15026  psrval  15099  fnpsr  15100  setsmsdsg  15630  cosz12  15931  sinpi  15936  sinhalfpilem  15942  coshalfpi  15948  sincosq1lem  15976  tangtx  15989  sincos4thpi  15991  tan4thpi  15992  sincos6thpi  15993  sincos3rdpi  15994  pigt3  15995  logltb  16026  log2tlbndlog2  16139  ppiublem1  16192  ppiublem2  16193  lgsdir2lem4  16248  lgsdir2lem5  16249