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

Theorem simp1bi 1007
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 1004 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    /\ w3a 973
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 975
This theorem is referenced by:  limord  4378  smores2  6270  smofvon2dm  6272  smofvon  6275  errel  6518  lincmb01cmp  9947  iccf1o  9948  elfznn0  10057  elfzouz  10094  ef01bndlem  11706  sin01bnd  11707  cos01bnd  11708  sin01gt0  11711  cos01gt0  11712  sin02gt0  11713  eulerthlema  12171  modprm0  12195  gzcn  12311  coseq00topi  13509  coseq0negpitopi  13510  cosq34lt1  13524  cos11  13527  nconstwlpolemgt0  14055
  Copyright terms: Public domain W3C validator