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

Theorem simp2i 1064
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 1055 . 2 ((𝜑𝜓𝜒) → 𝜓)
31, 2ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  hartogslem2  8331  harwdom  8378  divalglem6  14959  strleun  15799  birthdaylem3  24480  birthday  24481  divsqrsum  24508  harmonicbnd  24530  lgslem4  24825  lgscllem  24829  lgsdir2lem2  24851  mulog2sum  25026  vmalogdivsum2  25027  siilem2  27091  h2hva  27215  h2hsm  27216  hhssabloi  27503  elunop2  28256  wallispilem3  38960  wallispilem4  38961
  Copyright terms: Public domain W3C validator