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

Theorem simp1i 966
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
simp1i  |-  ph

Proof of Theorem simp1i
StepHypRef Expression
1 3simp1i.1 . 2  |-  ( ph  /\ 
ps  /\  ch )
2 simp1 957 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
31, 2ax-mp 8 1  |-  ph
Colors of variables: wff set class
Syntax hints:    /\ w3a 936
This theorem is referenced by:  find  4862  hartogslem2  7504  harwdom  7550  divalglem6  12910  structfn  13474  strleun  13551  birthday  20785  divsqrsumf  20811  emcl  20833  lgslem4  21075  lgscllem  21079  lgsdir2lem2  21100  mulog2sumlem1  21220  siilem2  22345  h2hva  22469  h2hsm  22470  elunop2  23508  wallispilem3  27773  wallispilem4  27774
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