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

Theorem simp1i 1134
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 1131 . 2 ((𝜑𝜓𝜒) → 𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  find  7257  hartogslem2  8615  harwdom  8662  divalglem6  15343  structfn  16096  strleun  16194  rmodislmod  19153  birthday  24901  divsqrsumf  24927  emcl  24949  lgslem4  25245  lgscllem  25249  lgsdir2lem2  25271  mulog2sumlem1  25443  siilem2  28037  h2hva  28161  h2hsm  28162  elunop2  29202  wallispilem3  40805  wallispilem4  40806
  Copyright terms: Public domain W3C validator