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

Theorem simp3i 1007
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 998 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
31, 2ax-mp 5 1  |-  ch
Colors of variables: wff setvar class
Syntax hints:    /\ w3a 973
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 975
This theorem is referenced by:  hartogslem2  7968  harwdom  8016  divalglem6  13915  structfn  14503  strleun  14585  dfrelog  22709  log2ub  23036  birthdaylem3  23039  birthday  23040  divsqrtsum2  23068  harmonicbnd2  23090  lgslem4  23330  lgscllem  23334  lgsdir2lem2  23355  lgsdir2lem3  23356  mulog2sumlem1  23475  siilem2  25471  h2hva  25595  h2hsm  25596  h2hnm  25597  elunop2  26636  wallispilem3  31395  wallispilem4  31396
  Copyright terms: Public domain W3C validator