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

Theorem simpri 449
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 448 . 2  |-  ( (
ph  /\  ps )  ->  ps )
31, 2ax-mp 8 1  |-  ps
Colors of variables: wff set class
Syntax hints:    /\ wa 359
This theorem is referenced by:  exan  1899  tfr2b  6624  rdgdmlim  6642  oeoa  6807  oeoe  6809  ordtypelem3  7453  ordtypelem5  7455  ordtypelem6  7456  ordtypelem7  7457  ordtypelem9  7459  r1fin  7663  r1tr  7666  r1ordg  7668  r1ord3g  7669  r1pwss  7674  r1val1  7676  rankwflemb  7683  r1elwf  7686  rankr1ai  7688  rankdmr1  7691  rankr1ag  7692  rankr1bg  7693  pwwf  7697  unwf  7700  rankr1clem  7710  rankr1c  7711  rankval3b  7716  rankonidlem  7718  onssr1  7721  rankeq0b  7750  alephsuc2  7925  ackbij2  8087  wunom  8559  negiso  9948  infmsup  9950  om2uzoi  11258  faclbnd4lem1  11547  hashgt12el  11645  hashgt12el2  11646  hashunlei  11647  hashsslei  11648  cos01bnd  12750  cos1bnd  12751  cos2bnd  12752  sincos2sgn  12758  sin4lt0  12759  egt2lt3  12768  divalglem9  12884  bitsinv  12923  strlemor1  13519  drngui  15804  iccpnfcnv  18930  xrhmph  18933  i1f1  19543  itg11  19544  dvcos  19828  sinpi  20332  sinhalfpilem  20335  coshalfpi  20338  sincosq1lem  20366  tangtx  20374  sincos4thpi  20382  tan4thpi  20383  sincos6thpi  20384  sincos3rdpi  20385  pige3  20386  logltb  20455  1cubrlem  20642  1cubr  20643  log2tlbnd  20746  cxploglim2  20778  emcllem6  20800  emcllem7  20801  ppiublem1  20947  ppiublem2  20948  bposlem9  21037  lgsdir2lem4  21071  lgsdir2lem5  21072  chebbnd1lem2  21125  chebbnd1lem3  21126  chebbnd1  21127  dchrvmasumlema  21155  mulog2sumlem2  21190  pntlemb  21252  qdrng  21275  umgra1  21322  uslgra1  21353  2trllemE  21514  umgrabi  21666  normlem7tALT  22582  hhsssh  22730  shintcli  22792  chintcli  22794  omlsi  22867  qlaxr3i  23099  lnophm  23483  nmcopex  23493  nmcoplb  23494  nmbdfnlbi  23513  nmcfnex  23517  nmcfnlb  23518  hmopidmch  23617  hmopidmpj  23618  chirred  23859  redvr  24238  refld  24240  xrge0hmph  24279  qqh0  24329  qqh1  24330  zrhre  24346  qqhre  24347  mbfmvolf  24577  subfacval2  24834  erdszelem5  24842  erdszelem6  24843  erdszelem7  24844  erdszelem8  24845  ghomgrpilem1  25057  filnetlem3  26307  filnetlem4  26308  abcdtb  27766  abcdtc  27767  abcdtd  27768  uun0.1  28608
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator