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

Theorem simp1i 1068
 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 1059 . 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:  find  7041  hartogslem2  8395  harwdom  8442  divalglem6  15048  structfn  15800  strleun  15896  birthday  24588  divsqrsumf  24614  emcl  24636  lgslem4  24932  lgscllem  24936  lgsdir2lem2  24958  mulog2sumlem1  25130  siilem2  27568  h2hva  27692  h2hsm  27693  elunop2  28733  wallispilem3  39607  wallispilem4  39608
 Copyright terms: Public domain W3C validator