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

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

Proof of Theorem simpr1
StepHypRef Expression
1 simp1 943 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
21adantl 271 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  simplr1  985  simprr1  991  simp1r1  1039  simp2r1  1045  simp3r1  1051  3anandis  1283  isopolem  5593  caovlem2d  5829  tfrlemibacc  6083  tfrlemibfn  6085  tfr1onlembacc  6099  tfr1onlembfn  6101  tfrcllembacc  6112  tfrcllembfn  6114  eqsupti  6681  prmuloc2  7116  elioc2  9344  elico2  9345  elicc2  9346  fseq1p1m1  9496  elfz0ubfz0  9524  ico0  9661  seq3f1olemp  9919  seq3f1oleml  9920  ibcval5  10159  isumss2  10772  tanaddap  11017  dvds2ln  11094  divalglemeunn  11186  divalglemex  11187  divalglemeuneg  11188  qredeq  11343  findset  11723
  Copyright terms: Public domain W3C validator