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

Theorem simpr3 990
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 984 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 275 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
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:  simplr3  1026  simprr3  1032  simp1r3  1080  simp2r3  1086  simp3r3  1092  3anandis  1326  isopolem  5730  tfrlemibacc  6230  tfrlemibxssdm  6231  tfrlemibfn  6232  tfr1onlembacc  6246  tfr1onlembxssdm  6247  tfr1onlembfn  6248  tfrcllembacc  6259  tfrcllembxssdm  6260  tfrcllembfn  6261  elfir  6868  prloc  7322  prmuloc2  7398  ltntri  7913  eluzuzle  9357  xlesubadd  9695  elioc2  9748  elico2  9749  elicc2  9750  fseq1p1m1  9904  seq3f1olemp  10305  seq3f1oleml  10306  bcval5  10540  hashdifpr  10597  isumss2  11193  tanaddap  11480  dvds2ln  11560  divalglemeunn  11652  divalglemex  11653  divalglemeuneg  11654  restopnb  12387  icnpimaex  12417  cnptopresti  12444  psmettri  12536  isxmet2d  12554  xmettri  12578  metrtri  12583  xmetres2  12585  bldisj  12607  blss2ps  12612  blss2  12613  xmstri2  12676  mstri2  12677  xmstri  12678  mstri  12679  xmstri3  12680  mstri3  12681  msrtri  12682  comet  12705  bdbl  12709  xmetxp  12713  dvconst  12867
  Copyright terms: Public domain W3C validator