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

Theorem simpr2 946
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpr2  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ch )

Proof of Theorem simpr2
StepHypRef Expression
1 simp2 940 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
21adantl 271 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  simplr2  982  simprr2  988  simp1r2  1036  simp2r2  1042  simp3r2  1048  3anandis  1279  isopolem  5492  tfrlemibacc  5975  tfrlemibfn  5977  tfr1onlembacc  5991  tfr1onlembfn  5993  tfrcllembacc  6004  tfrcllembfn  6006  prltlu  6739  prdisj  6744  prmuloc2  6819  eluzuzle  8708  elioc2  9035  elico2  9036  elicc2  9037  fseq1p1m1  9187  fz0fzelfz0  9215  ibcval5  9787  dvds2ln  10373  divalglemeunn  10465  divalglemex  10466  divalglemeuneg  10467
  Copyright terms: Public domain W3C validator