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  5033  fcof1  5475  fliftfun  5488  addcmpblnq  6655  mulcmpblnq  6656  ordpipqqs  6662  enq0tr  6722  addcmpblnq0  6731  mulcmpblnq0  6732  nnnq0lem1  6734  addnq0mo  6735  mulnq0mo  6736  prarloclemcalc  6790  addlocpr  6824  distrlem4prl  6872  distrlem4pru  6873  addcmpblnr  7014  mulcmpblnrlemg  7015  mulcmpblnr  7016  prsrlem1  7017  addsrmo  7018  mulsrmo  7019  ltsrprg  7022  apreap  7790  apreim  7806  divdivdivap  7904  divsubdivap  7919  ledivdiv  8071  lediv12a  8075  exbtwnz  9373  iseqcaopr  9594  leexp2r  9663  recvguniq  10066  rsqrmo  10098  qredeu  10670  pw2dvdseu  10737
  Copyright terms: Public domain W3C validator