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

Theorem simp3i 1137
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 1134 . 2 ((𝜑𝜓𝜒) → 𝜒)
31, 2ax-mp 5 1 𝜒
Colors of variables: wff setvar class
Syntax hints:  w3a 1083
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 209  df-an 399  df-3an 1085
This theorem is referenced by:  hartogslem2  9001  harwdom  9048  divalglem6  15743  structfn  16494  strleun  16585  dfrelog  25143  log2ub  25521  birthdaylem3  25525  birthday  25526  divsqrtsum2  25554  harmonicbnd2  25576  lgslem4  25870  lgscllem  25874  lgsdir2lem2  25896  lgsdir2lem3  25897  mulog2sumlem1  26104  siilem2  28623  h2hva  28745  h2hsm  28746  h2hnm  28747  elunop2  29784  wallispilem3  42345  wallispilem4  42346
  Copyright terms: Public domain W3C validator