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

Theorem simp3bi 998
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 995 1  |-  ( ph  ->  th )
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  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  limuni  4318  smores2  6191  ersym  6441  ertr  6444  fvixp  6597  fiintim  6817  eluzle  9345  ef01bndlem  11470  sin01bnd  11471  cos01bnd  11472  sin01gt0  11475  ennnfonelemim  11944  reeff1oleme  12871  cosq14gt0  12926  cosq23lt0  12927  coseq0q4123  12928  coseq00topi  12929  coseq0negpitopi  12930  cosq34lt1  12944  cos02pilt1  12945  ioocosf1o  12948
  Copyright terms: Public domain W3C validator