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  7438  eninr  7439  pw1ne1  7589  negiso  9288  infrenegsupex  10004  xrnegiso  12047  infxrnegsupex  12048  cos01bnd  12544  cos1bnd  12545  cos2bnd  12546  sincos2sgn  12552  sin4lt0  12553  egt2lt3  12566  ssnnctlemct  13389  slotslfn  13430  strslfvd  13446  strslfv2d  13447  strslfv  13449  strslfv3  13450  strsl0  13453  setsslid  13455  setsslnid  13456  slotm  13467  rngplusgg  13544  rngmulrg  13545  srngplusgd  13555  srngmulrd  13556  srnginvld  13557  lmodplusgd  13573  lmodscad  13574  lmodvscad  13575  ipsaddgd  13585  ipsmulrd  13586  ipsscad  13587  ipsvscad  13588  ipsipd  13589  topgrpplusgd  13605  topgrptsetd  13606  prdsvallem  13674  imasex  13679  imasival  13680  imasbas  13681  imasplusg  13682  imasmulr  13683  prdsex  14256  prdsval  14257  prdssca  14259  prdsmulr  14262  fnmgp  14303  mgpvalg  14304  mgpex  14307  mgpbasg  14308  mgpscag  14310  mgptsetg  14311  mgpdsg  14313  mgpress  14314  ring1  14448  opprvalg  14458  opprex  14462  opprsllem  14463  rmodislmod  14772  sraval  14858  sralemg  14859  srascag  14863  sravscag  14864  sraipg  14865  sraex  14867  zlmval  15046  zlmlemg  15047  zlmmulrg  15050  zlmsca  15051  zlmvscag  15052  znmul  15061  psrval  15134  fnpsr  15135  setsmsdsg  15672  cosz12  15973  sinpi  15978  sinhalfpilem  15984  coshalfpi  15990  sincosq1lem  16018  tangtx  16031  sincos4thpi  16033  tan4thpi  16034  sincos6thpi  16035  sincos3rdpi  16036  pigt3  16037  logltb  16068  log2tlbndlog2  16181  ppiublem1  16252  ppiublem2  16253  bposlem9  16280  lgsdir2lem4  16316  lgsdir2lem5  16317