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

Theorem simpr3 912
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpr3  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )

Proof of Theorem simpr3
StepHypRef Expression
1 simp3 906 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 262 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97    /\ w3a 885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 887
This theorem is referenced by:  simplr3  948  simprr3  954  simp1r3  1002  simp2r3  1008  simp3r3  1014  3anandis  1237  isopolem  5461  tfrlemibacc  5940  tfrlemibxssdm  5941  tfrlemibfn  5942  prloc  6589  prmuloc2  6665  eluzuzle  8481  elioc2  8805  elico2  8806  elicc2  8807  fseq1p1m1  8956
  Copyright terms: Public domain W3C validator