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  6724  hartogslem2  7986  harwdom  8034  divalglem6  14067  structfn  14656  strleun  14741  birthday  23409  divsqrsumf  23435  emcl  23457  lgslem4  23699  lgscllem  23703  lgsdir2lem2  23724  mulog2sumlem1  23844  siilem2  25893  h2hva  26017  h2hsm  26018  elunop2  27058  wallispilem3  32010  wallispilem4  32011
  Copyright terms: Public domain W3C validator