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

Theorem simp2bi 1014
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 120 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp2d 1011 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  w3a 979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107
This theorem depends on definitions:  df-bi 117  df-3an 981
This theorem is referenced by:  0ellim  4412  smodm  6309  erdm  6562  ixpfn  6721  dif1en  6896  eluzelz  9554  elfz3nn0  10132  ef01bndlem  11781  sin01bnd  11782  cos01bnd  11783  sin01gt0  11786  gznegcl  12390  gzcjcl  12391  gzaddcl  12392  gzmulcl  12393  gzabssqcl  12396  4sqlem4a  12406  xpsff1o  12790  subgss  13078  rngmgp  13250  srgmgp  13282  ringmgp  13316  lmodring  13571  lmodprop2d  13624  reeff1oleme  14576  cosq14gt0  14636  cosq23lt0  14637  coseq0q4123  14638  coseq00topi  14639  coseq0negpitopi  14640  cosq34lt1  14654  cos02pilt1  14655  ioocosf1o  14658  2sqlem2  14845  2sqlem3  14847
  Copyright terms: Public domain W3C validator