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

Theorem simpr1 998
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 992 . 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 973
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 975
This theorem is referenced by:  simplr1  1034  simprr1  1040  simp1r1  1088  simp2r1  1094  simp3r1  1100  3anandis  1342  isopolem  5801  caovlem2d  6045  tfrlemibacc  6305  tfrlemibfn  6307  tfr1onlembacc  6321  tfr1onlembfn  6323  tfrcllembacc  6334  tfrcllembfn  6336  eqsupti  6973  prmuloc2  7529  ltntri  8047  elioc2  9893  elico2  9894  elicc2  9895  fseq1p1m1  10050  elfz0ubfz0  10081  ico0  10218  seq3f1olemp  10458  seq3f1oleml  10459  bcval5  10697  isumss2  11356  tanaddap  11702  dvds2ln  11786  divalglemeunn  11880  divalglemex  11881  divalglemeuneg  11882  qredeq  12050  pcdvdstr  12280  isstructr  12431  mndissubm  12697  icnpimaex  13005  cnptopresti  13032  upxp  13066  psmettri  13124  isxmet2d  13142  xmettri  13166  metrtri  13171  xmetres2  13173  bldisj  13195  blss2ps  13200  blss2  13201  xmstri2  13264  mstri2  13265  xmstri  13266  mstri  13267  xmstri3  13268  mstri3  13269  msrtri  13270  comet  13293  bdbl  13297  xmetxp  13301  dvconst  13455  findset  13980
  Copyright terms: Public domain W3C validator