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

Theorem simp3i 1070
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 1061 . 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  8393  harwdom  8440  divalglem6  15040  structfn  15792  strleun  15888  dfrelog  24211  log2ub  24571  birthdaylem3  24575  birthday  24576  divsqrtsum2  24604  harmonicbnd2  24626  lgslem4  24920  lgscllem  24924  lgsdir2lem2  24946  lgsdir2lem3  24947  mulog2sumlem1  25118  siilem2  27547  h2hva  27671  h2hsm  27672  h2hnm  27673  elunop2  28712  wallispilem3  39559  wallispilem4  39560
  Copyright terms: Public domain W3C validator