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  1922  tfr2b  7062  rdgdmlim  7080  oeoa  7243  oeoe  7245  ordtypelem3  7941  ordtypelem5  7943  ordtypelem6  7944  ordtypelem7  7945  ordtypelem9  7947  r1fin  8187  r1tr  8190  r1ordg  8192  r1ord3g  8193  r1pwss  8198  r1val1  8200  rankwflemb  8207  r1elwf  8210  rankr1ai  8212  rankdmr1  8215  rankr1ag  8216  rankr1bg  8217  pwwf  8221  unwf  8224  rankr1clem  8234  rankr1c  8235  rankval3b  8240  rankonidlem  8242  onssr1  8245  rankeq0b  8274  alephsuc2  8457  ackbij2  8619  wunom  9094  negiso  10515  infmsup  10517  om2uzoi  12030  faclbnd4lem1  12335  hashgt12el  12442  hashgt12el2  12443  hashunlei  12444  hashsslei  12445  cos01bnd  13778  cos1bnd  13779  cos2bnd  13780  sincos2sgn  13786  sin4lt0  13787  egt2lt3  13796  divalglem9  13914  bitsinv  13953  strlemor1  14578  drngui  17185  redvr  18420  refld  18422  recrng  18424  iccpnfcnv  21179  xrhmph  21182  i1f1  21832  itg11  21833  dvcos  22119  sinpi  22584  sinhalfpilem  22589  coshalfpi  22595  sincosq1lem  22623  tangtx  22631  sincos4thpi  22639  tan4thpi  22640  sincos6thpi  22641  sincos3rdpi  22642  pige3  22643  logltb  22712  1cubrlem  22900  1cubr  22901  log2tlbnd  23004  cxploglim2  23036  emcllem6  23058  emcllem7  23059  ppiublem1  23205  ppiublem2  23206  bposlem9  23295  lgsdir2lem4  23329  lgsdir2lem5  23330  chebbnd1lem2  23383  chebbnd1lem3  23384  chebbnd1  23385  dchrvmasumlema  23413  mulog2sumlem2  23448  pntlemb  23510  qdrng  23533  umgra1  24002  uslgra1  24048  2trllemE  24231  umgrabi  24659  normlem7tALT  25712  hhsssh  25861  shintcli  25923  chintcli  25925  omlsi  25998  qlaxr3i  26230  lnophm  26614  nmcopex  26624  nmcoplb  26625  nmbdfnlbi  26644  nmcfnex  26648  nmcfnlb  26649  hmopidmch  26748  hmopidmpj  26749  chirred  26990  xrge0hmph  27550  qqh0  27601  qqh1  27602  rerrext  27626  zrhre  27633  qqhre  27634  mbfmvolf  27877  subfacval2  28271  erdszelem5  28279  erdszelem6  28280  erdszelem7  28281  erdszelem8  28282  ghomgrpilem1  28500  filnetlem3  29801  filnetlem4  29802  islptre  31161  fourierdlem62  31469  fourierdlem68  31475  abcdtb  31585  abcdtc  31586  abcdtd  31587  zlmodzxzsubm  32012  zlmodzxzldep  32186  ldepsnlinclem1  32187  ldepsnlinclem2  32188  uun0.1  32655