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

Theorem simpr3 957
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 951 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 273 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 932
This theorem is referenced by:  simplr3  993  simprr3  999  simp1r3  1047  simp2r3  1053  simp3r3  1059  3anandis  1293  isopolem  5655  tfrlemibacc  6153  tfrlemibxssdm  6154  tfrlemibfn  6155  tfr1onlembacc  6169  tfr1onlembxssdm  6170  tfr1onlembfn  6171  tfrcllembacc  6182  tfrcllembxssdm  6183  tfrcllembfn  6184  prloc  7200  prmuloc2  7276  ltntri  7761  eluzuzle  9184  xlesubadd  9507  elioc2  9560  elico2  9561  elicc2  9562  fseq1p1m1  9715  seq3f1olemp  10116  seq3f1oleml  10117  bcval5  10350  hashdifpr  10407  isumss2  11001  tanaddap  11244  dvds2ln  11321  divalglemeunn  11413  divalglemex  11414  divalglemeuneg  11415  restopnb  12132  icnpimaex  12161  cnptopresti  12188  psmettri  12258  isxmet2d  12276  xmettri  12300  metrtri  12305  xmetres2  12307  bldisj  12329  blss2ps  12334  blss2  12335  xmstri2  12398  mstri2  12399  xmstri  12400  mstri  12401  xmstri3  12402  mstri3  12403  msrtri  12404  comet  12427  bdbl  12431  dvconst  12534
  Copyright terms: Public domain W3C validator