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  4442  smores2  6379  ersym  6631  ertr  6634  fvixp  6789  en2  6911  fiintim  7027  eluzle  9659  ef01bndlem  12009  sin01bnd  12010  cos01bnd  12011  sin01gt0  12015  gznegcl  12640  gzcjcl  12641  gzaddcl  12642  gzmulcl  12643  gzabssqcl  12646  4sqlem4a  12656  ennnfonelemim  12737  prdsbasprj  13056  xpsff1o  13123  subggrp  13455  srgdilem  13673  srgrz  13688  srglz  13689  ringdilem  13716  ringsrg  13751  subrngss  13904  lmodlema  13996  reeff1oleme  15186  cosq14gt0  15246  cosq23lt0  15247  coseq0q4123  15248  coseq00topi  15249  coseq0negpitopi  15250  cosq34lt1  15264  cos02pilt1  15265  ioocosf1o  15268  2sqlem2  15534  2sqlem3  15536
  Copyright terms: Public domain W3C validator