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  7258  harwdom  7304  divalglem6  12597  structfn  13161  strleun  13238  dfrelog  19923  log2ub  20245  birthdaylem3  20248  birthday  20249  divsqrsum2  20277  harmonicbnd2  20298  lgslem4  20538  lgscllem  20542  lgsdir2lem2  20563  lgsdir2lem3  20564  mulog2sumlem1  20683  siilem2  21430  h2hva  21554  h2hsm  21555  h2hnm  21556  elunop2  22593  wallispilem3  27816  wallispilem4  27817  wallispilem5  27818
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