Theorem simpri 460

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

Syntax hints:   /\ wa 367

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 369

This theorem is referenced by:  exan  1981  tfr2b  6983  rdgdmlim  7001  oeoa  7164  oeoe  7166  ordtypelem3  7860  ordtypelem5  7862  ordtypelem6  7863  ordtypelem7  7864  ordtypelem9  7866  r1fin  8104  r1tr  8107  r1ordg  8109  r1ord3g  8110  r1pwss  8115  r1val1  8117  rankwflemb  8124  r1elwf  8127  rankr1ai  8129  rankdmr1  8132  rankr1ag  8133  rankr1bg  8134  pwwf  8138  unwf  8141  rankr1clem  8151  rankr1c  8152  rankval3b  8157  rankonidlem  8159  onssr1  8162  rankeq0b  8191  alephsuc2  8374  ackbij2  8536  wunom  9009  negiso  10435  infmsup  10437  om2uzoi  11969  faclbnd4lem1  12273  hashgt12el  12385  hashgt12el2  12386  hashunlei  12387  hashsslei  12388  cos01bnd  13923  cos1bnd  13924  cos2bnd  13925  sincos2sgn  13931  sin4lt0  13932  egt2lt3  13941  divalglem9  14061  bitsinv  14100  strlemor1  14729  drngui  17515  redvr  18744  refld  18746  recrng  18748  iccpnfcnv  21529  xrhmph  21532  i1f1  22182  itg11  22183  dvcos  22469  sinpi  22935  sinhalfpilem  22941  coshalfpi  22947  sincosq1lem  22975  tangtx  22983  sincos4thpi  22991  tan4thpi  22992  sincos6thpi  22993  sincos3rdpi  22994  pige3  22995  logltb  23072  1cubrlem  23288  1cubr  23289  log2tlbnd  23392  cxploglim2  23425  emcllem6  23447  emcllem7  23448  ppiublem1  23594  ppiublem2  23595  bposlem9  23684  lgsdir2lem4  23718  lgsdir2lem5  23719  chebbnd1lem2  23772  chebbnd1lem3  23773  chebbnd1  23774  dchrvmasumlema  23802  mulog2sumlem2  23837  pntlemb  23899  qdrng  23922  umgra1  24447  uslgra1  24493  2trllemE  24676  umgrabi  25104  normlem7tALT  26153  hhsssh  26302  shintcli  26364  chintcli  26366  omlsi  26439  qlaxr3i  26671  lnophm  27054  nmcopex  27064  nmcoplb  27065  nmbdfnlbi  27084  nmcfnex  27088  nmcfnlb  27089  hmopidmch  27188  hmopidmpj  27189  chirred  27430  xrge0hmph  28068  qqh0  28118  qqh1  28119  rerrext  28143  zrhre  28150  qqhre  28151  mbfmvolf  28393  subfacval2  28820  erdszelem5  28828  erdszelem6  28829  erdszelem7  28830  erdszelem8  28831  ghomgrpilem1  29214  filnetlem3  30364  filnetlem4  30365  fourierdlem62  32117  fourierdlem68  32123  abcdtb  32284  abcdtc  32285  abcdtd  32286  zlmodzxzsubm  33148  zlmodzxzldep  33305  ldepsnlinclem1  33306  ldepsnlinclem2  33307  uun0.1  33915