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  9285  infrenegsupex  9994  xrnegiso  12028  infxrnegsupex  12029  cos01bnd  12525  cos1bnd  12526  cos2bnd  12527  sincos2sgn  12533  sin4lt0  12534  egt2lt3  12547  ssnnctlemct  13337  slotslfn  13378  strslfvd  13394  strslfv2d  13395  strslfv  13397  strslfv3  13398  strsl0  13401  setsslid  13403  setsslnid  13404  slotm  13415  rngplusgg  13491  rngmulrg  13492  srngplusgd  13502  srngmulrd  13503  srnginvld  13504  lmodplusgd  13520  lmodscad  13521  lmodvscad  13522  ipsaddgd  13532  ipsmulrd  13533  ipsscad  13534  ipsvscad  13535  ipsipd  13536  topgrpplusgd  13552  topgrptsetd  13553  prdsvallem  13621  imasex  13626  imasival  13627  imasbas  13628  imasplusg  13629  imasmulr  13630  prdsex  14172  prdsval  14173  prdssca  14175  prdsmulr  14178  fnmgp  14219  mgpvalg  14220  mgpex  14223  mgpbasg  14224  mgpscag  14226  mgptsetg  14227  mgpdsg  14229  mgpress  14230  ring1  14364  opprvalg  14374  opprex  14378  opprsllem  14379  rmodislmod  14688  sraval  14774  sralemg  14775  srascag  14779  sravscag  14780  sraipg  14781  sraex  14783  zlmval  14962  zlmlemg  14963  zlmmulrg  14966  zlmsca  14967  zlmvscag  14968  znmul  14977  psrval  15050  fnpsr  15051  setsmsdsg  15581  cosz12  15881  sinpi  15886  sinhalfpilem  15892  coshalfpi  15898  sincosq1lem  15926  tangtx  15939  sincos4thpi  15941  tan4thpi  15942  sincos6thpi  15943  sincos3rdpi  15944  pigt3  15945  logltb  15975  log2tlbndlog2  16082  lgsdir2lem4  16150  lgsdir2lem5  16151