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

Theorem simp1bi 961
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
simp1bi  |-  ( ph  ->  ps )

Proof of Theorem simp1bi
StepHypRef Expression
1 3simp1bi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
21biimpi 119 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp1d 958 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    /\ w3a 927
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-3an 929
This theorem is referenced by:  limord  4246  smores2  6097  smofvon2dm  6099  smofvon  6102  errel  6341  lincmb01cmp  9569  iccf1o  9570  elfznn0  9677  elfzouz  9711  ef01bndlem  11212  sin01bnd  11213  cos01bnd  11214  sin01gt0  11217  cos01gt0  11218  sin02gt0  11219
  Copyright terms: Public domain W3C validator