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

Theorem simprlr 505
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simprlr  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )

Proof of Theorem simprlr
StepHypRef Expression
1 simpr 108 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antrl 474 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
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 is referenced by:  imain  5096  fcof1  5562  fliftfun  5575  sbthlemi6  6671  sbthlemi8  6673  addcmpblnq  6926  mulcmpblnq  6927  ordpipqqs  6933  enq0tr  6993  addcmpblnq0  7002  mulcmpblnq0  7003  nnnq0lem1  7005  addnq0mo  7006  mulnq0mo  7007  prarloclemcalc  7061  addlocpr  7095  distrlem4prl  7143  distrlem4pru  7144  addcmpblnr  7285  mulcmpblnrlemg  7286  mulcmpblnr  7287  prsrlem1  7288  addsrmo  7289  mulsrmo  7290  ltsrprg  7293  apreap  8064  apreim  8080  divdivdivap  8180  divsubdivap  8195  ledivdiv  8351  lediv12a  8355  exbtwnz  9662  iseqcaopr  9912  leexp2r  10009  zfz1iso  10246  recvguniq  10428  rsqrmo  10460  isummolem2  10772  qredeu  11357  pw2dvdseu  11424
  Copyright terms: Public domain W3C validator