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

Theorem simpr1 988
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 982 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
21adantl 275 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  simplr1  1024  simprr1  1030  simp1r1  1078  simp2r1  1084  simp3r1  1090  3anandis  1329  isopolem  5774  caovlem2d  6015  tfrlemibacc  6275  tfrlemibfn  6277  tfr1onlembacc  6291  tfr1onlembfn  6293  tfrcllembacc  6304  tfrcllembfn  6306  eqsupti  6942  prmuloc2  7489  ltntri  8007  elioc2  9846  elico2  9847  elicc2  9848  fseq1p1m1  10002  elfz0ubfz0  10033  ico0  10170  seq3f1olemp  10410  seq3f1oleml  10411  bcval5  10648  isumss2  11301  tanaddap  11647  dvds2ln  11731  divalglemeunn  11824  divalglemex  11825  divalglemeuneg  11826  qredeq  11988  isstructr  12275  icnpimaex  12681  cnptopresti  12708  upxp  12742  psmettri  12800  isxmet2d  12818  xmettri  12842  metrtri  12847  xmetres2  12849  bldisj  12871  blss2ps  12876  blss2  12877  xmstri2  12940  mstri2  12941  xmstri  12942  mstri  12943  xmstri3  12944  mstri3  12945  msrtri  12946  comet  12969  bdbl  12973  xmetxp  12977  dvconst  13131  findset  13591
  Copyright terms: Public domain W3C validator