Theorem simpri 459

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 458	. 2 |- ( ( ph /\ ps ) -> ps )
3	1, 2	ax-mp 5	1 |- ps

Syntax hints:   /\ wa 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  exan  1899  tfr2b  6841  rdgdmlim  6859  oeoa  7024  oeoe  7026  ordtypelem3  7722  ordtypelem5  7724  ordtypelem6  7725  ordtypelem7  7726  ordtypelem9  7728  r1fin  7968  r1tr  7971  r1ordg  7973  r1ord3g  7974  r1pwss  7979  r1val1  7981  rankwflemb  7988  r1elwf  7991  rankr1ai  7993  rankdmr1  7996  rankr1ag  7997  rankr1bg  7998  pwwf  8002  unwf  8005  rankr1clem  8015  rankr1c  8016  rankval3b  8021  rankonidlem  8023  onssr1  8026  rankeq0b  8055  alephsuc2  8238  ackbij2  8400  wunom  8874  negiso  10293  infmsup  10295  om2uzoi  11761  faclbnd4lem1  12052  hashgt12el  12156  hashgt12el2  12157  hashunlei  12158  hashsslei  12159  cos01bnd  13452  cos1bnd  13453  cos2bnd  13454  sincos2sgn  13460  sin4lt0  13461  egt2lt3  13470  divalglem9  13587  bitsinv  13626  strlemor1  14247  drngui  16761  redvr  17888  refld  17890  recrng  17892  iccpnfcnv  20357  xrhmph  20360  i1f1  21009  itg11  21010  dvcos  21296  sinpi  21804  sinhalfpilem  21809  coshalfpi  21815  sincosq1lem  21843  tangtx  21851  sincos4thpi  21859  tan4thpi  21860  sincos6thpi  21861  sincos3rdpi  21862  pige3  21863  logltb  21932  1cubrlem  22120  1cubr  22121  log2tlbnd  22224  cxploglim2  22256  emcllem6  22278  emcllem7  22279  ppiublem1  22425  ppiublem2  22426  bposlem9  22515  lgsdir2lem4  22549  lgsdir2lem5  22550  chebbnd1lem2  22603  chebbnd1lem3  22604  chebbnd1  22605  dchrvmasumlema  22633  mulog2sumlem2  22668  pntlemb  22730  qdrng  22753  umgra1  23082  uslgra1  23113  2trllemE  23274  umgrabi  23426  normlem7tALT  24343  hhsssh  24492  shintcli  24554  chintcli  24556  omlsi  24629  qlaxr3i  24861  lnophm  25245  nmcopex  25255  nmcoplb  25256  nmbdfnlbi  25275  nmcfnex  25279  nmcfnlb  25280  hmopidmch  25379  hmopidmpj  25380  chirred  25621  xrge0hmph  26215  qqh0  26266  qqh1  26267  rerrext  26291  zrhre  26298  qqhre  26299  mbfmvolf  26534  subfacval2  26922  erdszelem5  26930  erdszelem6  26931  erdszelem7  26932  erdszelem8  26933  ghomgrpilem1  27150  filnetlem3  28442  filnetlem4  28443  abcdtb  29780  abcdtc  29781  abcdtd  29782  zlmodzxzsubm  30587  zlmodzxzldep  30752  ldepsnlinclem1  30753  ldepsnlinclem2  30754  uun0.1  31210