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

Theorem simp2i 1001
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 992 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
31, 2ax-mp 5 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    /\ w3a 968
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 970
This theorem is referenced by:  hartogslem2  7957  harwdom  8005  divalglem6  13904  strleun  14574  birthdaylem3  23004  birthday  23005  divsqrsum  23032  harmonicbnd  23054  lgslem4  23295  lgscllem  23299  lgsdir2lem2  23320  mulog2sum  23443  vmalogdivsum2  23444  siilem2  25293  h2hva  25417  h2hsm  25418  hhssabloi  25704  elunop2  26458  wallispilem3  31186  wallispilem4  31187
  Copyright terms: Public domain W3C validator