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 206  df-an 395  df-3an 1086
This theorem is referenced by:  hartogslem2  9568  harwdom  9616  divalglem6  16378  strleun  17129  oppcbas  17702  sratset  21086  srads  21089  tngvsca  24604  birthdaylem3  26930  birthday  26931  divsqrsum  26959  harmonicbnd  26981  lgslem4  27278  lgscllem  27282  lgsdir2lem2  27304  mulog2sum  27515  vmalogdivsum2  27516  siilem2  30734  h2hva  30856  h2hsm  30857  hhssabloi  31144  elunop2  31895  1fldgenq  33108  zlmds  33694  zlmtset  33696  wallispilem3  45593  wallispilem4  45594  prstcbas  48259
  Copyright terms: Public domain W3C validator