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

Theorem simp3i 1007
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
simp3i  |-  ch

Proof of Theorem simp3i
StepHypRef Expression
1 3simp1i.1 . 2  |-  ( ph  /\ 
ps  /\  ch )
2 simp3 998 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
31, 2ax-mp 5 1  |-  ch
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:  hartogslem2  7986  harwdom  8034  divalglem6  14068  structfn  14657  strleun  14742  dfrelog  23079  log2ub  23406  birthdaylem3  23409  birthday  23410  divsqrtsum2  23438  harmonicbnd2  23460  lgslem4  23700  lgscllem  23704  lgsdir2lem2  23725  lgsdir2lem3  23726  mulog2sumlem1  23845  siilem2  25894  h2hva  26018  h2hsm  26019  h2hnm  26020  elunop2  27059  wallispilem3  32052  wallispilem4  32053
  Copyright terms: Public domain W3C validator