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

Theorem simpri 448
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 447 . 2  |-  ( (
ph  /\  ps )  ->  ps )
31, 2ax-mp 8 1  |-  ps
Colors of variables: wff set class
Syntax hints:    /\ wa 358
This theorem is referenced by:  tfr2b  6412  rdgdmlim  6430  oeoa  6595  oeoe  6597  ordtypelem3  7235  ordtypelem5  7237  ordtypelem6  7238  ordtypelem7  7239  ordtypelem9  7241  r1fin  7445  r1tr  7448  r1ordg  7450  r1ord3g  7451  r1pwss  7456  r1val1  7458  rankwflemb  7465  r1elwf  7468  rankr1ai  7470  rankdmr1  7473  rankr1ag  7474  rankr1bg  7475  pwwf  7479  unwf  7482  rankr1clem  7492  rankr1c  7493  rankval3b  7498  rankonidlem  7500  onssr1  7503  rankeq0b  7532  alephsuc2  7707  ackbij2  7869  wunom  8342  negiso  9730  infmsup  9732  om2uzoi  11018  faclbnd4lem1  11306  hashunlei  11377  hashsslei  11378  cos01bnd  12466  cos1bnd  12467  cos2bnd  12468  sincos2sgn  12474  sin4lt0  12475  egt2lt3  12484  divalglem9  12600  bitsinv  12639  strlemor1  13235  drngui  15518  iccpnfcnv  18442  xrhmph  18445  i1f1  19045  itg11  19046  dvcos  19330  sinpi  19831  sinhalfpilem  19834  coshalfpi  19837  sincosq1lem  19865  tangtx  19873  sincos4thpi  19881  tan4thpi  19882  sincos6thpi  19883  sincos3rdpi  19884  pige3  19885  logltb  19953  1cubrlem  20137  1cubr  20138  log2tlbnd  20241  cxploglim2  20273  emcllem6  20294  emcllem7  20295  ppiublem1  20441  ppiublem2  20442  bposlem9  20531  lgsdir2lem4  20565  lgsdir2lem5  20566  chebbnd1lem2  20619  chebbnd1lem3  20620  chebbnd1  20621  dchrvmasumlema  20649  mulog2sumlem2  20684  pntlemb  20746  qdrng  20769  normlem7tALT  21698  hhsssh  21846  shintcli  21908  chintcli  21910  omlsi  21983  qlaxr3i  22215  lnophm  22599  nmcopex  22609  nmcoplb  22610  nmbdfnlbi  22629  nmcfnex  22633  nmcfnlb  22634  hmopidmch  22733  hmopidmpj  22734  chirred  22975  xrge0hmph  23314  mbfmvolf  23571  subfacval2  23718  erdszelem5  23726  erdszelem6  23727  erdszelem7  23728  erdszelem8  23729  umgra1  23878  umgrabi  23907  ghomgrpilem1  23992  cntrset  25602  filnetlem3  26329  filnetlem4  26330  stirlinglem13  27835  uslgra1  28118  uun0.1  28553
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 177  df-an 360
  Copyright terms: Public domain W3C validator