Theorem simpri 462

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 461	. 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  1901  tfr2b  6860  rdgdmlim  6878  oeoa  7041  oeoe  7043  ordtypelem3  7739  ordtypelem5  7741  ordtypelem6  7742  ordtypelem7  7743  ordtypelem9  7745  r1fin  7985  r1tr  7988  r1ordg  7990  r1ord3g  7991  r1pwss  7996  r1val1  7998  rankwflemb  8005  r1elwf  8008  rankr1ai  8010  rankdmr1  8013  rankr1ag  8014  rankr1bg  8015  pwwf  8019  unwf  8022  rankr1clem  8032  rankr1c  8033  rankval3b  8038  rankonidlem  8040  onssr1  8043  rankeq0b  8072  alephsuc2  8255  ackbij2  8417  wunom  8892  negiso  10311  infmsup  10313  om2uzoi  11783  faclbnd4lem1  12074  hashgt12el  12178  hashgt12el2  12179  hashunlei  12180  hashsslei  12181  cos01bnd  13475  cos1bnd  13476  cos2bnd  13477  sincos2sgn  13483  sin4lt0  13484  egt2lt3  13493  divalglem9  13610  bitsinv  13649  strlemor1  14270  drngui  16843  redvr  18052  refld  18054  recrng  18056  iccpnfcnv  20521  xrhmph  20524  i1f1  21173  itg11  21174  dvcos  21460  sinpi  21925  sinhalfpilem  21930  coshalfpi  21936  sincosq1lem  21964  tangtx  21972  sincos4thpi  21980  tan4thpi  21981  sincos6thpi  21982  sincos3rdpi  21983  pige3  21984  logltb  22053  1cubrlem  22241  1cubr  22242  log2tlbnd  22345  cxploglim2  22377  emcllem6  22399  emcllem7  22400  ppiublem1  22546  ppiublem2  22547  bposlem9  22636  lgsdir2lem4  22670  lgsdir2lem5  22671  chebbnd1lem2  22724  chebbnd1lem3  22725  chebbnd1  22726  dchrvmasumlema  22754  mulog2sumlem2  22789  pntlemb  22851  qdrng  22874  umgra1  23265  uslgra1  23296  2trllemE  23457  umgrabi  23609  normlem7tALT  24526  hhsssh  24675  shintcli  24737  chintcli  24739  omlsi  24812  qlaxr3i  25044  lnophm  25428  nmcopex  25438  nmcoplb  25439  nmbdfnlbi  25458  nmcfnex  25462  nmcfnlb  25463  hmopidmch  25562  hmopidmpj  25563  chirred  25804  xrge0hmph  26367  qqh0  26418  qqh1  26419  rerrext  26443  zrhre  26450  qqhre  26451  mbfmvolf  26686  subfacval2  27080  erdszelem5  27088  erdszelem6  27089  erdszelem7  27090  erdszelem8  27091  ghomgrpilem1  27309  filnetlem3  28606  filnetlem4  28607  abcdtb  29942  abcdtc  29943  abcdtd  29944  zlmodzxzsubm  30761  zlmodzxzldep  31051  ldepsnlinclem1  31052  ldepsnlinclem2  31053  uun0.1  31516