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

Theorem simp2i 967
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 958 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
31, 2ax-mp 8 1  |-  ps
Colors of variables: wff set class
Syntax hints:    /\ w3a 936
This theorem is referenced by:  hartogslem2  7445  harwdom  7491  divalglem6  12845  strleun  13486  birthdaylem3  20659  birthday  20660  divsqrsum  20687  harmonicbnd  20709  lgslem4  20950  lgscllem  20954  lgsdir2lem2  20975  mulog2sum  21098  vmalogdivsum2  21099  siilem2  22201  h2hva  22325  h2hsm  22326  hhssabloi  22610  elunop2  23364  wallispilem3  27484  wallispilem4  27485
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator