Theorem simpri 478

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

Syntax hints:   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  exan  1788  exanOLD  1789  exanOLDOLD  2169  tfr2b  7492  rdgdmlim  7513  oeoa  7677  oeoe  7679  ordtypelem3  8425  ordtypelem5  8427  ordtypelem6  8428  ordtypelem7  8429  ordtypelem9  8431  r1fin  8636  r1tr  8639  r1ordg  8641  r1ord3g  8642  r1pwss  8647  r1val1  8649  rankwflemb  8656  r1elwf  8659  rankr1ai  8661  rankdmr1  8664  rankr1ag  8665  rankr1bg  8666  pwwf  8670  unwf  8673  rankr1clem  8683  rankr1c  8684  rankval3b  8689  rankonidlem  8691  onssr1  8694  rankeq0b  8723  alephsuc2  8903  ackbij2  9065  wunom  9542  negiso  11003  infrenegsup  11006  om2uzoi  12754  faclbnd4lem1  13080  hashunlei  13212  hashsslei  13213  hashle2pr  13259  cos01bnd  14916  cos1bnd  14917  cos2bnd  14918  sincos2sgn  14924  sin4lt0  14925  egt2lt3  14934  divalglem9  15124  bitsinv  15170  strlemor1OLD  15969  drngui  18753  redvr  19963  refld  19965  recrng  19967  iccpnfcnv  22743  xrhmph  22746  recvs  22946  qcvs  22947  i1f1  23457  itg11  23458  dvcos  23746  sinpi  24209  sinhalfpilem  24215  coshalfpi  24221  sincosq1lem  24249  tangtx  24257  sincos4thpi  24265  tan4thpi  24266  sincos6thpi  24267  sincos3rdpi  24268  pige3  24269  logltb  24346  1cubrlem  24568  1cubr  24569  log2tlbnd  24672  cxploglim2  24705  emcllem6  24727  emcllem7  24728  ppiublem1  24927  ppiublem2  24928  bposlem9  25017  lgsdir2lem4  25053  lgsdir2lem5  25054  chebbnd1lem2  25159  chebbnd1lem3  25160  chebbnd1  25161  dchrvmasumlema  25189  mulog2sumlem2  25224  pntlemb  25286  qdrng  25309  upgrbi  25988  upgr1elem  26007  usgrexmpledg  26154  ntrl2v2e  27018  frgrwopreg2  27183  normlem7tALT  27976  hhsssh  28126  shintcli  28188  chintcli  28190  omlsi  28263  qlaxr3i  28495  lnophm  28878  nmcopex  28888  nmcoplb  28889  nmbdfnlbi  28908  nmcfnex  28912  nmcfnlb  28913  hmopidmch  29012  hmopidmpj  29013  chirred  29254  xrge0hmph  29978  qqh0  30028  qqh1  30029  rerrext  30053  zrhre  30063  qqhre  30064  mbfmvolf  30328  hgt750lem  30729  subfacval2  31169  erdszelem5  31177  erdszelem6  31178  erdszelem7  31179  erdszelem8  31180  filnetlem3  32375  filnetlem4  32376  bj-genr  32591  bj-genl  32592  bj-genan  32593  uun0.1  39005  pssnssi  39283  fourierdlem62  40385  fourierdlem68  40391  abcdtb  41093  abcdtc  41094  abcdtd  41095  nabctnabc  41098  zlmodzxzsubm  42137  zlmodzxzldep  42293  ldepsnlinclem1  42294  ldepsnlinclem2  42295