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

Theorem simp3bi 1016
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 120 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp3d 1013 1  |-  ( ph  ->  th )
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  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  limuni  4414  smores2  6319  ersym  6571  ertr  6574  fvixp  6729  fiintim  6957  eluzle  9570  ef01bndlem  11796  sin01bnd  11797  cos01bnd  11798  sin01gt0  11801  gznegcl  12407  gzcjcl  12408  gzaddcl  12409  gzmulcl  12410  gzabssqcl  12413  4sqlem4a  12423  ennnfonelemim  12475  xpsff1o  12825  subggrp  13116  srgdilem  13323  srgrz  13338  srglz  13339  ringdilem  13366  ringsrg  13399  subrngss  13547  lmodlema  13608  reeff1oleme  14650  cosq14gt0  14710  cosq23lt0  14711  coseq0q4123  14712  coseq00topi  14713  coseq0negpitopi  14714  cosq34lt1  14728  cos02pilt1  14729  ioocosf1o  14732  2sqlem2  14920  2sqlem3  14922
  Copyright terms: Public domain W3C validator