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

Theorem simp1i 997
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 988 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    /\ w3a 965
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 967
This theorem is referenced by:  find  6612  hartogslem2  7869  harwdom  7917  divalglem6  13721  structfn  14306  strleun  14388  birthday  22482  divsqrsumf  22508  emcl  22530  lgslem4  22772  lgscllem  22776  lgsdir2lem2  22797  mulog2sumlem1  22917  siilem2  24405  h2hva  24529  h2hsm  24530  elunop2  25570  wallispilem3  30011  wallispilem4  30012
  Copyright terms: Public domain W3C validator