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

Theorem simp3bi 983
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
simp3bi  |-  ( ph  ->  th )

Proof of Theorem simp3bi
StepHypRef Expression
1 3simp1bi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
21biimpi 119 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp3d 980 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    /\ w3a 947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  limuni  4288  smores2  6159  ersym  6409  ertr  6412  fvixp  6565  fiintim  6785  eluzle  9306  ef01bndlem  11390  sin01bnd  11391  cos01bnd  11392  sin01gt0  11395  ennnfonelemim  11864  cosq14gt0  12840  cosq23lt0  12841  coseq0q4123  12842  coseq00topi  12843  coseq0negpitopi  12844  cosq34lt1  12858  cos02pilt1  12859
  Copyright terms: Public domain W3C validator