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

Theorem simp2i 1176
Description: Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
Hypothesis
Ref Expression
3simp1i.1 (𝜑𝜓𝜒)
Assertion
Ref Expression
simp2i 𝜓

Proof of Theorem simp2i
StepHypRef Expression
1 3simp1i.1 . 2 (𝜑𝜓𝜒)
2 simp2 1173 . 2 ((𝜑𝜓𝜒) → 𝜓)
31, 2ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  w3a 1113
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 199  df-an 387  df-3an 1115
This theorem is referenced by:  hartogslem2  8717  harwdom  8764  divalglem6  15495  strleun  16331  birthdaylem3  25093  birthday  25094  divsqrsum  25121  harmonicbnd  25143  lgslem4  25438  lgscllem  25442  lgsdir2lem2  25464  mulog2sum  25639  vmalogdivsum2  25640  siilem2  28262  h2hva  28386  h2hsm  28387  hhssabloi  28674  elunop2  29427  wallispilem3  41078  wallispilem4  41079
  Copyright terms: Public domain W3C validator