MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp3i Structured version   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  7504  harwdom  7550  divalglem6  12910  structfn  13474  strleun  13551  dfrelog  20455  log2ub  20781  birthdaylem3  20784  birthday  20785  divsqrsum2  20813  harmonicbnd2  20835  lgslem4  21075  lgscllem  21079  lgsdir2lem2  21100  lgsdir2lem3  21101  mulog2sumlem1  21220  siilem2  22345  h2hva  22469  h2hsm  22470  h2hnm  22471  elunop2  23508  wallispilem3  27783  wallispilem4  27784
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