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  713  mptxor  1444  sb4bor  1859  ordsoexmid  4618  eninl  7214  eninr  7215  pw1ne1  7360  negiso  9048  infrenegsupex  9735  xrnegiso  11648  infxrnegsupex  11649  cos01bnd  12144  cos1bnd  12145  cos2bnd  12146  sincos2sgn  12152  sin4lt0  12153  egt2lt3  12166  ssnnctlemct  12892  slotslfn  12933  strslfvd  12949  strslfv2d  12950  strslfv  12952  strslfv3  12953  strsl0  12956  setsslid  12958  setsslnid  12959  rngplusgg  13044  rngmulrg  13045  srngplusgd  13055  srngmulrd  13056  srnginvld  13057  lmodplusgd  13073  lmodscad  13074  lmodvscad  13075  ipsaddgd  13085  ipsmulrd  13086  ipsscad  13087  ipsvscad  13088  ipsipd  13089  topgrpplusgd  13105  topgrptsetd  13106  prdsex  13176  prdsvallem  13179  prdsval  13180  prdssca  13182  prdsmulr  13185  imasex  13212  imasival  13213  imasbas  13214  imasplusg  13215  imasmulr  13216  fnmgp  13759  mgpvalg  13760  mgpex  13762  mgpbasg  13763  mgpscag  13764  mgptsetg  13765  mgpdsg  13767  mgpress  13768  ring1  13896  opprvalg  13906  opprex  13910  opprsllem  13911  rmodislmod  14188  sraval  14274  sralemg  14275  srascag  14279  sravscag  14280  sraipg  14281  sraex  14283  zlmval  14464  zlmlemg  14465  zlmmulrg  14468  zlmsca  14469  zlmvscag  14470  znmul  14479  psrval  14503  fnpsr  14504  setsmsdsg  15027  cosz12  15327  sinpi  15332  sinhalfpilem  15338  coshalfpi  15344  sincosq1lem  15372  tangtx  15385  sincos4thpi  15387  tan4thpi  15388  sincos6thpi  15389  sincos3rdpi  15390  pigt3  15391  logltb  15421  lgsdir2lem4  15583  lgsdir2lem5  15584