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

Theorem simp2bi 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
simp2bi (𝜑𝜒)

Proof of Theorem simp2bi
StepHypRef Expression
1 3simp1bi.1 . . 3 (𝜑 ↔ (𝜓𝜒𝜃))
21biimpi 119 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp2d 994 1 (𝜑𝜒)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   ∧ w3a 962 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106 This theorem depends on definitions:  df-bi 116  df-3an 964 This theorem is referenced by:  0ellim  4320  smodm  6188  erdm  6439  ixpfn  6598  dif1en  6773  eluzelz  9342  elfz3nn0  9902  ef01bndlem  11470  sin01bnd  11471  cos01bnd  11472  sin01gt0  11475  cosq14gt0  12923  cosq23lt0  12924  coseq0q4123  12925  coseq00topi  12926  coseq0negpitopi  12927  cosq34lt1  12941  cos02pilt1  12942  ioocosf1o  12945
 Copyright terms: Public domain W3C validator