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

Theorem simpr3 947
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 941 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 271 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
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:  simplr3  983  simprr3  989  simp1r3  1037  simp2r3  1043  simp3r3  1049  3anandis  1279  isopolem  5492  tfrlemibacc  5975  tfrlemibxssdm  5976  tfrlemibfn  5977  tfr1onlembacc  5991  tfr1onlembxssdm  5992  tfr1onlembfn  5993  tfrcllembacc  6004  tfrcllembxssdm  6005  tfrcllembfn  6006  prloc  6743  prmuloc2  6819  eluzuzle  8708  elioc2  9035  elico2  9036  elicc2  9037  fseq1p1m1  9187  ibcval5  9787  dvds2ln  10373  divalglemeunn  10465  divalglemex  10466  divalglemeuneg  10467
  Copyright terms: Public domain W3C validator