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

Theorem simp3i 1092
 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 1083 . 2 ((𝜑𝜓𝜒) → 𝜒)
31, 2ax-mp 5 1 𝜒
 Colors of variables: wff setvar class Syntax hints:   ∧ w3a 1054 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 385  df-3an 1056 This theorem is referenced by:  hartogslem2  8489  harwdom  8536  divalglem6  15168  structfn  15921  strleun  16019  dfrelog  24357  log2ub  24721  birthdaylem3  24725  birthday  24726  divsqrtsum2  24754  harmonicbnd2  24776  lgslem4  25070  lgscllem  25074  lgsdir2lem2  25096  lgsdir2lem3  25097  mulog2sumlem1  25268  siilem2  27835  h2hva  27959  h2hsm  27960  h2hnm  27961  elunop2  29000  wallispilem3  40602  wallispilem4  40603
 Copyright terms: Public domain W3C validator