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

Theorem simp2i 998
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 989 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
31, 2ax-mp 5 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    /\ w3a 965
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 967
This theorem is referenced by:  hartogslem2  7858  harwdom  7906  divalglem6  13704  strleun  14370  birthdaylem3  22463  birthday  22464  divsqrsum  22491  harmonicbnd  22513  lgslem4  22754  lgscllem  22758  lgsdir2lem2  22779  mulog2sum  22902  vmalogdivsum2  22903  siilem2  24387  h2hva  24511  h2hsm  24512  hhssabloi  24798  elunop2  25552  wallispilem3  30000  wallispilem4  30001
  Copyright terms: Public domain W3C validator