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

Theorem simp1i 1131
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 1128 . 2 ((𝜑𝜓𝜒) → 𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  find  7596  hartogslem2  8995  harwdom  9042  divalglem6  15737  structfn  16488  strleun  16579  rmodislmod  19631  birthday  25459  divsqrsumf  25485  emcl  25507  lgslem4  25803  lgscllem  25807  lgsdir2lem2  25829  mulog2sumlem1  26037  siilem2  28556  h2hva  28678  h2hsm  28679  elunop2  29717  wallispilem3  42229  wallispilem4  42230
  Copyright terms: Public domain W3C validator