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

Theorem simp2i 1019
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 1010 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
31, 2ax-mp 5 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    /\ w3a 986
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 189  df-an 373  df-3an 988
This theorem is referenced by:  hartogslem2  8063  harwdom  8110  divalglem6  14390  strleun  15232  birthdaylem3  23891  birthday  23892  divsqrsum  23919  harmonicbnd  23941  lgslem4  24239  lgscllem  24243  lgsdir2lem2  24264  mulog2sum  24387  vmalogdivsum2  24388  siilem2  26505  h2hva  26639  h2hsm  26640  hhssabloi  26925  elunop2  27678  wallispilem3  37939  wallispilem4  37940
  Copyright terms: Public domain W3C validator