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

Theorem simp1i 1005
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 996 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    /\ w3a 973
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 975
This theorem is referenced by:  find  6703  hartogslem2  7964  harwdom  8012  divalglem6  13908  structfn  14496  strleun  14578  birthday  23009  divsqrsumf  23035  emcl  23057  lgslem4  23299  lgscllem  23303  lgsdir2lem2  23324  mulog2sumlem1  23444  siilem2  25440  h2hva  25564  h2hsm  25565  elunop2  26605  wallispilem3  31367  wallispilem4  31368
  Copyright terms: Public domain W3C validator