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

Theorem simp2i 1069
 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 1060 . 2 ((𝜑𝜓𝜒) → 𝜓)
31, 2ax-mp 5 1 𝜓
 Colors of variables: wff setvar class Syntax hints:   ∧ w3a 1036 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 197  df-an 386  df-3an 1038 This theorem is referenced by:  hartogslem2  8392  harwdom  8439  divalglem6  15045  strleun  15893  birthdaylem3  24580  birthday  24581  divsqrsum  24608  harmonicbnd  24630  lgslem4  24925  lgscllem  24929  lgsdir2lem2  24951  mulog2sum  25126  vmalogdivsum2  25127  siilem2  27556  h2hva  27680  h2hsm  27681  hhssabloi  27968  elunop2  28721  wallispilem3  39591  wallispilem4  39592
 Copyright terms: Public domain W3C validator