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

Theorem simp3i 966
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 957 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
31, 2ax-mp 8 1  |-  ch
Colors of variables: wff set class
Syntax hints:    /\ w3a 934
This theorem is referenced by:  hartogslem2  7274  harwdom  7320  divalglem6  12613  structfn  13177  strleun  13254  dfrelog  19939  log2ub  20261  birthdaylem3  20264  birthday  20265  divsqrsum2  20293  harmonicbnd2  20314  lgslem4  20554  lgscllem  20558  lgsdir2lem2  20579  lgsdir2lem3  20580  mulog2sumlem1  20699  siilem2  21446  h2hva  21570  h2hsm  21571  h2hnm  21572  elunop2  22609  wallispilem3  27919  wallispilem4  27920  wallispilem5  27921
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator