MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp1i 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  4811  hartogslem2  7446  harwdom  7492  divalglem6  12846  structfn  13410  strleun  13487  birthday  20661  divsqrsumf  20687  emcl  20709  lgslem4  20951  lgscllem  20955  lgsdir2lem2  20976  mulog2sumlem1  21096  siilem2  22202  h2hva  22326  h2hsm  22327  elunop2  23365  wallispilem3  27485  wallispilem4  27486
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