MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp2i Structured version   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  7504  harwdom  7550  divalglem6  12910  strleun  13551  birthdaylem3  20784  birthday  20785  divsqrsum  20812  harmonicbnd  20834  lgslem4  21075  lgscllem  21079  lgsdir2lem2  21100  mulog2sum  21223  vmalogdivsum2  21224  siilem2  22345  h2hva  22469  h2hsm  22470  hhssabloi  22754  elunop2  23508  wallispilem3  27783  wallispilem4  27784
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