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

Theorem simp3i 999
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 990 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
31, 2ax-mp 5 1  |-  ch
Colors of variables: wff setvar class
Syntax hints:    /\ w3a 965
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 967
This theorem is referenced by:  hartogslem2  7861  harwdom  7909  divalglem6  13713  structfn  14298  strleun  14379  dfrelog  22143  log2ub  22470  birthdaylem3  22473  birthday  22474  divsqrsum2  22502  harmonicbnd2  22524  lgslem4  22764  lgscllem  22768  lgsdir2lem2  22789  lgsdir2lem3  22790  mulog2sumlem1  22909  siilem2  24397  h2hva  24521  h2hsm  24522  h2hnm  24523  elunop2  25562  wallispilem3  30003  wallispilem4  30004
  Copyright terms: Public domain W3C validator