ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simp1bi GIF version

Theorem simp1bi 981
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
3simp1bi.1 (𝜑 ↔ (𝜓𝜒𝜃))
Assertion
Ref Expression
simp1bi (𝜑𝜓)

Proof of Theorem simp1bi
StepHypRef Expression
1 3simp1bi.1 . . 3 (𝜑 ↔ (𝜓𝜒𝜃))
21biimpi 119 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp1d 978 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  w3a 947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  limord  4287  smores2  6159  smofvon2dm  6161  smofvon  6164  errel  6406  lincmb01cmp  9754  iccf1o  9755  elfznn0  9862  elfzouz  9896  ef01bndlem  11390  sin01bnd  11391  cos01bnd  11392  sin01gt0  11395  cos01gt0  11396  sin02gt0  11397  coseq00topi  12843  coseq0negpitopi  12844  cosq34lt1  12858
  Copyright terms: Public domain W3C validator