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

Theorem simprlr 510
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 109 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antrl 479 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  imain  5173  fcof1  5650  fliftfun  5663  sbthlemi6  6816  sbthlemi8  6818  addcmpblnq  7139  mulcmpblnq  7140  ordpipqqs  7146  enq0tr  7206  addcmpblnq0  7215  mulcmpblnq0  7216  nnnq0lem1  7218  addnq0mo  7219  mulnq0mo  7220  prarloclemcalc  7274  addlocpr  7308  distrlem4prl  7356  distrlem4pru  7357  addcmpblnr  7511  mulcmpblnrlemg  7512  mulcmpblnr  7513  prsrlem1  7514  addsrmo  7515  mulsrmo  7516  ltsrprg  7519  apreap  8312  apreim  8328  divdivdivap  8433  divsubdivap  8448  ledivdiv  8605  lediv12a  8609  exbtwnz  9968  seq3caopr  10196  leexp2r  10287  zfz1iso  10524  recvguniq  10707  rsqrmo  10739  summodclem2  11091  qredeu  11674  pw2dvdseu  11741  epttop  12154  txdis1cn  12342  metequiv2  12560  cncfmptc  12646  cncfmptid  12647  addccncf  12650  negcncf  12652
  Copyright terms: Public domain W3C validator