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

Theorem simp2i 1137
Description: Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
Hypothesis
Ref Expression
3simp1i.1 (𝜑𝜓𝜒)
Assertion
Ref Expression
simp2i 𝜓

Proof of Theorem simp2i
StepHypRef Expression
1 3simp1i.1 . 2 (𝜑𝜓𝜒)
2 simp2 1134 . 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:  hartogslem2  9004  harwdom  9052  divalglem6  15747  strleun  16591  birthdaylem3  25546  birthday  25547  divsqrsum  25574  harmonicbnd  25596  lgslem4  25891  lgscllem  25895  lgsdir2lem2  25917  mulog2sum  26128  vmalogdivsum2  26129  siilem2  28642  h2hva  28764  h2hsm  28765  hhssabloi  29052  elunop2  29803  wallispilem3  42640  wallispilem4  42641
  Copyright terms: Public domain W3C validator