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

Theorem simp3i 1175
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 1172 . 2 ((𝜑𝜓𝜒) → 𝜒)
31, 2ax-mp 5 1 𝜒
Colors of variables: wff setvar class
Syntax hints:  w3a 1111
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 199  df-an 387  df-3an 1113
This theorem is referenced by:  hartogslem2  8724  harwdom  8771  divalglem6  15502  structfn  16246  strleun  16338  dfrelog  24718  log2ub  25096  birthdaylem3  25100  birthday  25101  divsqrtsum2  25129  harmonicbnd2  25151  lgslem4  25445  lgscllem  25449  lgsdir2lem2  25471  lgsdir2lem3  25472  mulog2sumlem1  25643  siilem2  28258  h2hva  28382  h2hsm  28383  h2hnm  28384  elunop2  29423  wallispilem3  41072  wallispilem4  41073
  Copyright terms: Public domain W3C validator