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

Theorem simp1i 1141
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 1138 . 2 ((𝜑𝜓𝜒) → 𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  w3a 1089
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 1091
This theorem is referenced by:  find  7683  findOLD  7684  hartogslem2  9172  harwdom  9220  divalglem6  15972  structfn  16722  strleun  16723  rmodislmod  19980  birthday  25850  divsqrsumf  25876  emcl  25898  lgslem4  26194  lgscllem  26198  lgsdir2lem2  26220  mulog2sumlem1  26428  siilem2  28946  h2hva  29068  h2hsm  29069  elunop2  30107  wallispilem3  43298  wallispilem4  43299  prstcbas  46036
  Copyright terms: Public domain W3C validator