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

Theorem simp3i 1019
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 1010 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
31, 2ax-mp 5 1  |-  ch
Colors of variables: wff setvar class
Syntax hints:    /\ w3a 985
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 189  df-an 373  df-3an 987
This theorem is referenced by:  hartogslem2  8058  harwdom  8105  divalglem6  14378  structfn  15134  strleun  15220  dfrelog  23515  log2ub  23875  birthdaylem3  23879  birthday  23880  divsqrtsum2  23908  harmonicbnd2  23930  lgslem4  24227  lgscllem  24231  lgsdir2lem2  24252  lgsdir2lem3  24253  mulog2sumlem1  24372  siilem2  26493  h2hva  26627  h2hsm  26628  h2hnm  26629  elunop2  27666  wallispilem3  37929  wallispilem4  37930
  Copyright terms: Public domain W3C validator