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

Theorem simpri 450
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 449 . 2  |-  ( (
ph  /\  ps )  ->  ps )
31, 2ax-mp 5 1  |-  ps
Colors of variables: wff set class
Syntax hints:    /\ wa 360
This theorem is referenced by:  exan  1906  tfr2b  6686  rdgdmlim  6704  oeoa  6869  oeoe  6871  ordtypelem3  7518  ordtypelem5  7520  ordtypelem6  7521  ordtypelem7  7522  ordtypelem9  7524  r1fin  7728  r1tr  7731  r1ordg  7733  r1ord3g  7734  r1pwss  7739  r1val1  7741  rankwflemb  7748  r1elwf  7751  rankr1ai  7753  rankdmr1  7756  rankr1ag  7757  rankr1bg  7758  pwwf  7762  unwf  7765  rankr1clem  7775  rankr1c  7776  rankval3b  7781  rankonidlem  7783  onssr1  7786  rankeq0b  7815  alephsuc2  7992  ackbij2  8154  wunom  8626  negiso  10015  infmsup  10017  om2uzoi  11326  faclbnd4lem1  11615  hashgt12el  11713  hashgt12el2  11714  hashunlei  11715  hashsslei  11716  cos01bnd  12818  cos1bnd  12819  cos2bnd  12820  sincos2sgn  12826  sin4lt0  12827  egt2lt3  12836  divalglem9  12952  bitsinv  12991  strlemor1  13587  drngui  15872  iccpnfcnv  19000  xrhmph  19003  i1f1  19611  itg11  19612  dvcos  19898  sinpi  20402  sinhalfpilem  20405  coshalfpi  20408  sincosq1lem  20436  tangtx  20444  sincos4thpi  20452  tan4thpi  20453  sincos6thpi  20454  sincos3rdpi  20455  pige3  20456  logltb  20525  1cubrlem  20712  1cubr  20713  log2tlbnd  20816  cxploglim2  20848  emcllem6  20870  emcllem7  20871  ppiublem1  21017  ppiublem2  21018  bposlem9  21107  lgsdir2lem4  21141  lgsdir2lem5  21142  chebbnd1lem2  21195  chebbnd1lem3  21196  chebbnd1  21197  dchrvmasumlema  21225  mulog2sumlem2  21260  pntlemb  21322  qdrng  21345  umgra1  21392  uslgra1  21423  2trllemE  21584  umgrabi  21736  normlem7tALT  22652  hhsssh  22800  shintcli  22862  chintcli  22864  omlsi  22937  qlaxr3i  23169  lnophm  23553  nmcopex  23563  nmcoplb  23564  nmbdfnlbi  23583  nmcfnex  23587  nmcfnlb  23588  hmopidmch  23687  hmopidmpj  23688  chirred  23929  redvr  24308  refld  24310  xrge0hmph  24349  qqh0  24399  qqh1  24400  zrhre  24416  qqhre  24417  mbfmvolf  24647  subfacval2  24904  erdszelem5  24912  erdszelem6  24913  erdszelem7  24914  erdszelem8  24915  ghomgrpilem1  25127  filnetlem3  26447  filnetlem4  26448  abcdtb  27905  abcdtc  27906  abcdtd  27907  uun0.1  28988
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 179  df-an 362
  Copyright terms: Public domain W3C validator