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

Theorem simp1i 1173
Description: Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
Hypothesis
Ref Expression
3simp1i.1 (𝜑𝜓𝜒)
Assertion
Ref Expression
simp1i 𝜑

Proof of Theorem simp1i
StepHypRef Expression
1 3simp1i.1 . 2 (𝜑𝜓𝜒)
2 simp1 1170 . 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:  find  7357  hartogslem2  8724  harwdom  8771  divalglem6  15502  structfn  16246  strleun  16338  rmodislmod  19294  birthday  25101  divsqrsumf  25127  emcl  25149  lgslem4  25445  lgscllem  25449  lgsdir2lem2  25471  mulog2sumlem1  25643  siilem2  28258  h2hva  28382  h2hsm  28383  elunop2  29423  wallispilem3  41072  wallispilem4  41073
  Copyright terms: Public domain W3C validator