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

Theorem simp2i 1006
Description: Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
Hypothesis
Ref Expression
3simp1i.1  |-  ( ph  /\ 
ps  /\  ch )
Assertion
Ref Expression
simp2i  |-  ps

Proof of Theorem simp2i
StepHypRef Expression
1 3simp1i.1 . 2  |-  ( ph  /\ 
ps  /\  ch )
2 simp2 997 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
31, 2ax-mp 5 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    /\ w3a 973
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  df-3an 975
This theorem is referenced by:  hartogslem2  7986  harwdom  8034  divalglem6  14068  strleun  14742  birthdaylem3  23409  birthday  23410  divsqrsum  23437  harmonicbnd  23459  lgslem4  23700  lgscllem  23704  lgsdir2lem2  23725  mulog2sum  23848  vmalogdivsum2  23849  siilem2  25894  h2hva  26018  h2hsm  26019  hhssabloi  26305  elunop2  27059  wallispilem3  32052  wallispilem4  32053
  Copyright terms: Public domain W3C validator