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

Theorem simp2bi 997
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 994 1  |-  ( ph  ->  ch )
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
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  0ellim  4320  smodm  6188  erdm  6439  ixpfn  6598  dif1en  6773  eluzelz  9342  elfz3nn0  9902  ef01bndlem  11470  sin01bnd  11471  cos01bnd  11472  sin01gt0  11475  reeff1oleme  12871  cosq14gt0  12926  cosq23lt0  12927  coseq0q4123  12928  coseq00topi  12929  coseq0negpitopi  12930  cosq34lt1  12944  cos02pilt1  12945  ioocosf1o  12948
  Copyright terms: Public domain W3C validator