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

Theorem simp2bi 1013
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
3simp1bi.1  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
Assertion
Ref Expression
simp2bi  |-  ( ph  ->  ch )

Proof of Theorem simp2bi
StepHypRef Expression
1 3simp1bi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
21biimpi 120 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp2d 1010 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105    /\ w3a 978
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 980
This theorem is referenced by:  0ellim  4397  smodm  6289  erdm  6542  ixpfn  6701  dif1en  6876  eluzelz  9533  elfz3nn0  10110  ef01bndlem  11757  sin01bnd  11758  cos01bnd  11759  sin01gt0  11762  gznegcl  12365  gzcjcl  12366  gzaddcl  12367  gzmulcl  12368  gzabssqcl  12371  4sqlem4a  12381  subgss  12965  srgmgp  13082  ringmgp  13116  reeff1oleme  14064  cosq14gt0  14124  cosq23lt0  14125  coseq0q4123  14126  coseq00topi  14127  coseq0negpitopi  14128  cosq34lt1  14142  cos02pilt1  14143  ioocosf1o  14146  2sqlem2  14322  2sqlem3  14324
  Copyright terms: Public domain W3C validator