Theorem simpri 464

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

Syntax hints:   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  exan  2052  tfr2b  7111  rdgdmlim  7132  oeoa  7295  oeoe  7297  ordtypelem3  8032  ordtypelem5  8034  ordtypelem6  8035  ordtypelem7  8036  ordtypelem9  8038  r1fin  8241  r1tr  8244  r1ordg  8246  r1ord3g  8247  r1pwss  8252  r1val1  8254  rankwflemb  8261  r1elwf  8264  rankr1ai  8266  rankdmr1  8269  rankr1ag  8270  rankr1bg  8271  pwwf  8275  unwf  8278  rankr1clem  8288  rankr1c  8289  rankval3b  8294  rankonidlem  8296  onssr1  8299  rankeq0b  8328  alephsuc2  8508  ackbij2  8670  wunom  9142  negiso  10584  infrenegsup  10588  infmsupOLD  10589  om2uzoi  12166  faclbnd4lem1  12475  hashgt12el  12592  hashgt12el2  12593  hashunlei  12594  hashsslei  12595  cos01bnd  14233  cos1bnd  14234  cos2bnd  14235  sincos2sgn  14241  sin4lt0  14242  egt2lt3  14251  divalglem9  14374  divalglem9OLD  14375  bitsinv  14415  strlemor1  15210  drngui  17974  redvr  19178  refld  19180  recrng  19182  iccpnfcnv  21965  xrhmph  21968  i1f1  22641  itg11  22642  dvcos  22928  sinpi  23405  sinhalfpilem  23411  coshalfpi  23417  sincosq1lem  23445  tangtx  23453  sincos4thpi  23461  tan4thpi  23462  sincos6thpi  23463  sincos3rdpi  23464  pige3  23465  logltb  23542  1cubrlem  23760  1cubr  23761  log2tlbnd  23864  cxploglim2  23897  emcllem6  23919  emcllem7  23920  ppiublem1  24123  ppiublem2  24124  bposlem9  24213  lgsdir2lem4  24247  lgsdir2lem5  24248  chebbnd1lem2  24301  chebbnd1lem3  24302  chebbnd1  24303  dchrvmasumlema  24331  mulog2sumlem2  24366  pntlemb  24428  qdrng  24451  umgra1  25046  uslgra1  25092  2trllemE  25276  umgrabi  25704  normlem7tALT  26765  hhsssh  26913  shintcli  26975  chintcli  26977  omlsi  27050  qlaxr3i  27282  lnophm  27665  nmcopex  27675  nmcoplb  27676  nmbdfnlbi  27695  nmcfnex  27699  nmcfnlb  27700  hmopidmch  27799  hmopidmpj  27800  chirred  28041  xrge0hmph  28731  qqh0  28781  qqh1  28782  rerrext  28806  zrhre  28816  qqhre  28817  mbfmvolf  29081  subfacval2  29903  erdszelem5  29911  erdszelem6  29912  erdszelem7  29913  erdszelem8  29914  ghomgrpilem1  30296  filnetlem3  31029  filnetlem4  31030  uun0.1  37159  fourierdlem62  38026  fourierdlem68  38032  abcdtb  38508  abcdtc  38509  abcdtd  38510  nabctnabc  38513  upgr1elem  39186  usgrexmpledg  39317  zlmodzxzsubm  40127  zlmodzxzldep  40284  ldepsnlinclem1  40285  ldepsnlinclem2  40286