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

Theorem simp1bi 996
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 993 1  |-  ( ph  ->  ps )
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
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  limord  4317  smores2  6191  smofvon2dm  6193  smofvon  6196  errel  6438  lincmb01cmp  9793  iccf1o  9794  elfznn0  9901  elfzouz  9935  ef01bndlem  11470  sin01bnd  11471  cos01bnd  11472  sin01gt0  11475  cos01gt0  11476  sin02gt0  11477  coseq00topi  12926  coseq0negpitopi  12927  cosq34lt1  12941  cos11  12944
  Copyright terms: Public domain W3C validator