MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpri Structured version   Unicode version

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
StepHypRef Expression
1 simpri.1 . 2  |-  ( ph  /\ 
ps )
2 simpr 461 . 2  |-  ( (
ph  /\  ps )  ->  ps )
31, 2ax-mp 5 1  |-  ps
Colors of variables: wff setvar class
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  1959  tfr2b  7067  rdgdmlim  7085  oeoa  7248  oeoe  7250  ordtypelem3  7948  ordtypelem5  7950  ordtypelem6  7951  ordtypelem7  7952  ordtypelem9  7954  r1fin  8194  r1tr  8197  r1ordg  8199  r1ord3g  8200  r1pwss  8205  r1val1  8207  rankwflemb  8214  r1elwf  8217  rankr1ai  8219  rankdmr1  8222  rankr1ag  8223  rankr1bg  8224  pwwf  8228  unwf  8231  rankr1clem  8241  rankr1c  8242  rankval3b  8247  rankonidlem  8249  onssr1  8252  rankeq0b  8281  alephsuc2  8464  ackbij2  8626  wunom  9101  negiso  10526  infmsup  10528  om2uzoi  12048  faclbnd4lem1  12353  hashgt12el  12463  hashgt12el2  12464  hashunlei  12465  hashsslei  12466  cos01bnd  13903  cos1bnd  13904  cos2bnd  13905  sincos2sgn  13911  sin4lt0  13912  egt2lt3  13921  divalglem9  14041  bitsinv  14080  strlemor1  14706  drngui  17381  redvr  18631  refld  18633  recrng  18635  iccpnfcnv  21422  xrhmph  21425  i1f1  22075  itg11  22076  dvcos  22362  sinpi  22828  sinhalfpilem  22834  coshalfpi  22840  sincosq1lem  22868  tangtx  22876  sincos4thpi  22884  tan4thpi  22885  sincos6thpi  22886  sincos3rdpi  22887  pige3  22888  logltb  22962  1cubrlem  23150  1cubr  23151  log2tlbnd  23254  cxploglim2  23286  emcllem6  23308  emcllem7  23309  ppiublem1  23455  ppiublem2  23456  bposlem9  23545  lgsdir2lem4  23579  lgsdir2lem5  23580  chebbnd1lem2  23633  chebbnd1lem3  23634  chebbnd1  23635  dchrvmasumlema  23663  mulog2sumlem2  23698  pntlemb  23760  qdrng  23783  umgra1  24304  uslgra1  24350  2trllemE  24533  umgrabi  24961  normlem7tALT  26014  hhsssh  26163  shintcli  26225  chintcli  26227  omlsi  26300  qlaxr3i  26532  lnophm  26916  nmcopex  26926  nmcoplb  26927  nmbdfnlbi  26946  nmcfnex  26950  nmcfnlb  26951  hmopidmch  27050  hmopidmpj  27051  chirred  27292  xrge0hmph  27892  qqh0  27943  qqh1  27944  rerrext  27968  zrhre  27975  qqhre  27976  mbfmvolf  28215  subfacval2  28609  erdszelem5  28617  erdszelem6  28618  erdszelem7  28619  erdszelem8  28620  ghomgrpilem1  29003  filnetlem3  30174  filnetlem4  30175  fourierdlem62  31905  fourierdlem68  31911  abcdtb  32072  abcdtc  32073  abcdtd  32074  zlmodzxzsubm  32816  zlmodzxzldep  32975  ldepsnlinclem1  32976  ldepsnlinclem2  32977  uun0.1  33443
  Copyright terms: Public domain W3C validator