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

Theorem simp3bi 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
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 1011 1  |-  ( ph  ->  th )
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  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  limuni  4397  smores2  6295  ersym  6547  ertr  6550  fvixp  6703  fiintim  6928  eluzle  9540  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  sin01gt0  11769  gznegcl  12373  gzcjcl  12374  gzaddcl  12375  gzmulcl  12376  gzabssqcl  12379  4sqlem4a  12389  ennnfonelemim  12425  xpsff1o  12768  subggrp  13037  srgdilem  13152  srgrz  13167  srglz  13168  ringdilem  13195  ringsrg  13224  lmodlema  13382  reeff1oleme  14196  cosq14gt0  14256  cosq23lt0  14257  coseq0q4123  14258  coseq00topi  14259  coseq0negpitopi  14260  cosq34lt1  14274  cos02pilt1  14275  ioocosf1o  14278  2sqlem2  14465  2sqlem3  14467
  Copyright terms: Public domain W3C validator