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

Theorem simp3i 968
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 959 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
31, 2ax-mp 8 1  |-  ch
Colors of variables: wff set class
Syntax hints:    /\ w3a 936
This theorem is referenced by:  hartogslem2  7438  harwdom  7484  divalglem6  12838  structfn  13402  strleun  13479  dfrelog  20323  log2ub  20649  birthdaylem3  20652  birthday  20653  divsqrsum2  20681  harmonicbnd2  20703  lgslem4  20943  lgscllem  20947  lgsdir2lem2  20968  lgsdir2lem3  20969  mulog2sumlem1  21088  siilem2  22194  h2hva  22318  h2hsm  22319  h2hnm  22320  elunop2  23357  wallispilem3  27477  wallispilem4  27478
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