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

Theorem simpr3 1005
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 999 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 277 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  simplr3  1041  simprr3  1047  simp1r3  1095  simp2r3  1101  simp3r3  1107  3anandis  1347  isopolem  5817  tfrlemibacc  6321  tfrlemibxssdm  6322  tfrlemibfn  6323  tfr1onlembacc  6337  tfr1onlembxssdm  6338  tfr1onlembfn  6339  tfrcllembacc  6350  tfrcllembxssdm  6351  tfrcllembfn  6352  elfir  6966  prloc  7478  prmuloc2  7554  ltntri  8072  eluzuzle  9522  xlesubadd  9867  elioc2  9920  elico2  9921  elicc2  9922  fseq1p1m1  10077  seq3f1olemp  10485  seq3f1oleml  10486  bcval5  10724  hashdifpr  10781  isumss2  11382  tanaddap  11728  dvds2ln  11812  divalglemeunn  11906  divalglemex  11907  divalglemeuneg  11908  grpsubadd  12844  grpaddsubass  12846  grpsubsub4  12849  grppnpcan2  12850  grpnpncan  12851  grpnnncan2  12853  mulgnndir  12897  mulgnn0dir  12898  mulgnnass  12903  mulgnn0ass  12904  mulgass  12905  cmn32  12931  cmn12  12933  abladdsub  12942  ablsubsub23  12952  srgdilem  12975  srgass  12977  ringdilem  13018  ringass  13022  opprring  13071  mulgass3  13076  unitgrp  13107  dvrass  13130  restopnb  13341  icnpimaex  13371  cnptopresti  13398  psmettri  13490  isxmet2d  13508  xmettri  13532  metrtri  13537  xmetres2  13539  bldisj  13561  blss2ps  13566  blss2  13567  xmstri2  13630  mstri2  13631  xmstri  13632  mstri  13633  xmstri3  13634  mstri3  13635  msrtri  13636  comet  13659  bdbl  13663  xmetxp  13667  dvconst  13821
  Copyright terms: Public domain W3C validator