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

Theorem simp3i 1136
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 1133 . 2 ((𝜑𝜓𝜒) → 𝜒)
31, 2ax-mp 5 1 𝜒
Colors of variables: wff setvar class
Syntax hints:  w3a 1072
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 1074
This theorem is referenced by:  hartogslem2  8616  harwdom  8663  divalglem6  15344  structfn  16097  strleun  16195  dfrelog  24533  log2ub  24897  birthdaylem3  24901  birthday  24902  divsqrtsum2  24930  harmonicbnd2  24952  lgslem4  25246  lgscllem  25250  lgsdir2lem2  25272  lgsdir2lem3  25273  mulog2sumlem1  25444  siilem2  28038  h2hva  28162  h2hsm  28163  h2hnm  28164  elunop2  29203  wallispilem3  40806  wallispilem4  40807
  Copyright terms: Public domain W3C validator