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:  exan  1890  tfr2b  6554  rdgdmlim  6572  oeoa  6737  oeoe  6739  ordtypelem3  7382  ordtypelem5  7384  ordtypelem6  7385  ordtypelem7  7386  ordtypelem9  7388  r1fin  7592  r1tr  7595  r1ordg  7597  r1ord3g  7598  r1pwss  7603  r1val1  7605  rankwflemb  7612  r1elwf  7615  rankr1ai  7617  rankdmr1  7620  rankr1ag  7621  rankr1bg  7622  pwwf  7626  unwf  7629  rankr1clem  7639  rankr1c  7640  rankval3b  7645  rankonidlem  7647  onssr1  7650  rankeq0b  7679  alephsuc2  7854  ackbij2  8016  wunom  8489  negiso  9877  infmsup  9879  om2uzoi  11182  faclbnd4lem1  11471  hashgt12el  11569  hashgt12el2  11570  hashunlei  11571  hashsslei  11572  cos01bnd  12674  cos1bnd  12675  cos2bnd  12676  sincos2sgn  12682  sin4lt0  12683  egt2lt3  12692  divalglem9  12808  bitsinv  12847  strlemor1  13443  drngui  15728  iccpnfcnv  18657  xrhmph  18660  i1f1  19260  itg11  19261  dvcos  19545  sinpi  20049  sinhalfpilem  20052  coshalfpi  20055  sincosq1lem  20083  tangtx  20091  sincos4thpi  20099  tan4thpi  20100  sincos6thpi  20101  sincos3rdpi  20102  pige3  20103  logltb  20172  1cubrlem  20359  1cubr  20360  log2tlbnd  20463  cxploglim2  20495  emcllem6  20517  emcllem7  20518  ppiublem1  20664  ppiublem2  20665  bposlem9  20754  lgsdir2lem4  20788  lgsdir2lem5  20789  chebbnd1lem2  20842  chebbnd1lem3  20843  chebbnd1  20844  dchrvmasumlema  20872  mulog2sumlem2  20907  pntlemb  20969  qdrng  20992  umgra1  21039  uslgra1  21070  normlem7tALT  22011  hhsssh  22159  shintcli  22221  chintcli  22223  omlsi  22296  qlaxr3i  22528  lnophm  22912  nmcopex  22922  nmcoplb  22923  nmbdfnlbi  22942  nmcfnex  22946  nmcfnlb  22947  hmopidmch  23046  hmopidmpj  23047  chirred  23288  redvr  23639  refld  23640  xrge0hmph  23673  qqh0  23840  qqh1  23841  qqhghm  23844  qqhrhm  23845  zrhre  23851  qqhre  23852  mbfmvolf  24079  subfacval2  24321  erdszelem5  24329  erdszelem6  24330  erdszelem7  24331  erdszelem8  24332  umgrabi  24494  ghomgrpilem1  24579  filnetlem3  25836  filnetlem4  25837  stirlinglem13  27341  uun0.1  28315
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