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

Theorem simp2bi 1013
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 120 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp2d 1010 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105    /\ w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  0ellim  4400  smodm  6295  erdm  6548  ixpfn  6707  dif1en  6882  eluzelz  9540  elfz3nn0  10118  ef01bndlem  11767  sin01bnd  11768  cos01bnd  11769  sin01gt0  11772  gznegcl  12376  gzcjcl  12377  gzaddcl  12378  gzmulcl  12379  gzabssqcl  12382  4sqlem4a  12392  xpsff1o  12774  subgss  13040  srgmgp  13157  ringmgp  13191  lmodring  13391  lmodprop2d  13444  reeff1oleme  14333  cosq14gt0  14393  cosq23lt0  14394  coseq0q4123  14395  coseq00topi  14396  coseq0negpitopi  14397  cosq34lt1  14411  cos02pilt1  14412  ioocosf1o  14415  2sqlem2  14602  2sqlem3  14604
  Copyright terms: Public domain W3C validator