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

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

Proof of Theorem simp3i
StepHypRef Expression
1 3simp1i.1 . 2 (𝜑𝜓𝜒)
2 simp3 1135 . 2 ((𝜑𝜓𝜒) → 𝜒)
31, 2ax-mp 5 1 𝜒
Colors of variables: wff setvar class
Syntax hints:  w3a 1084
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 206  df-an 395  df-3an 1086
This theorem is referenced by:  hartogslem2  9572  harwdom  9620  divalglem6  16380  structfn  17130  strleun  17131  oppchomfval  17699  sratset  21079  srads  21082  tngip  24580  dfrelog  26517  log2ub  26899  birthdaylem3  26903  birthday  26904  divsqrtsum2  26933  harmonicbnd2  26955  lgslem4  27251  lgscllem  27255  lgsdir2lem2  27277  lgsdir2lem3  27278  mulog2sumlem1  27485  siilem2  30680  h2hva  30802  h2hsm  30803  h2hnm  30804  elunop2  31841  wallispilem3  45457  wallispilem4  45458  prstchomval  48131
  Copyright terms: Public domain W3C validator