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

Theorem simp2bi 982
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
simp2bi  |-  ( ph  ->  ch )

Proof of Theorem simp2bi
StepHypRef Expression
1 3simp1bi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
21biimpi 119 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp2d 979 1  |-  ( ph  ->  ch )
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
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  0ellim  4290  smodm  6156  erdm  6407  ixpfn  6566  dif1en  6741  eluzelz  9303  elfz3nn0  9863  ef01bndlem  11390  sin01bnd  11391  cos01bnd  11392  sin01gt0  11395  cosq14gt0  12840  cosq23lt0  12841  coseq0q4123  12842  coseq00topi  12843  coseq0negpitopi  12844  cosq34lt1  12858  cos02pilt1  12859
  Copyright terms: Public domain W3C validator