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

Theorem simp1bi 997
 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 994 1 (𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   ∧ w3a 963 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 965 This theorem is referenced by:  limord  4328  smores2  6203  smofvon2dm  6205  smofvon  6208  errel  6450  lincmb01cmp  9845  iccf1o  9846  elfznn0  9954  elfzouz  9988  ef01bndlem  11535  sin01bnd  11536  cos01bnd  11537  sin01gt0  11540  cos01gt0  11541  sin02gt0  11542  coseq00topi  13000  coseq0negpitopi  13001  cosq34lt1  13015  cos11  13018  nconstwlpolemgt0  13477
 Copyright terms: Public domain W3C validator