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

Theorem simp1bi 1014
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
simp1bi  |-  ( ph  ->  ps )

Proof of Theorem simp1bi
StepHypRef Expression
1 3simp1bi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
21biimpi 120 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp1d 1011 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105    /\ w3a 980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  limord  4413  smores2  6319  smofvon2dm  6321  smofvon  6324  errel  6568  lincmb01cmp  10033  iccf1o  10034  elfznn0  10144  elfzouz  10181  ef01bndlem  11796  sin01bnd  11797  cos01bnd  11798  sin01gt0  11801  cos01gt0  11802  sin02gt0  11803  eulerthlema  12262  modprm0  12286  gzcn  12404  subgbas  13117  subgrcl  13118  rngabl  13289  srgcmn  13320  ringgrp  13355  subrngrcl  13550  lmodgrp  13610  coseq00topi  14713  coseq0negpitopi  14714  cosq34lt1  14728  cos11  14731  nconstwlpolemgt0  15271
  Copyright terms: Public domain W3C validator