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

Theorem simp1i 1136
 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 1133 . 2 ((𝜑𝜓𝜒) → 𝜑)
31, 2ax-mp 5 1 𝜑
 Colors of variables: wff setvar class Syntax hints:   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  find  7598  findOLD  7599  hartogslem2  9000  harwdom  9048  divalglem6  15745  structfn  16498  strleun  16589  rmodislmod  19697  birthday  25538  divsqrsumf  25564  emcl  25586  lgslem4  25882  lgscllem  25886  lgsdir2lem2  25908  mulog2sumlem1  26116  siilem2  28633  h2hva  28755  h2hsm  28756  elunop2  29794  wallispilem3  42575  wallispilem4  42576
 Copyright terms: Public domain W3C validator