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

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

Proof of Theorem simprll
StepHypRef Expression
1 simpl 106 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antrl 467 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  imain  5009  fcof1  5451  mpt20  5602  eroveu  6228  addcmpblnq  6523  mulcmpblnq  6524  ordpipqqs  6530  addcmpblnq0  6599  mulcmpblnq0  6600  nnnq0lem1  6602  prarloclemcalc  6658  addlocpr  6692  distrlem4prl  6740  distrlem4pru  6741  ltpopr  6751  addcmpblnr  6882  mulcmpblnrlemg  6883  mulcmpblnr  6884  prsrlem1  6885  ltsrprg  6890  apreap  7652  apreim  7668  divdivdivap  7764  divmuleqap  7768  divadddivap  7778  divsubdivap  7779  ledivdiv  7931  lediv12a  7935  qbtwnz  9208  iseqcaopr  9406  leexp2r  9474  recvguniq  9822  rsqrmo  9854  pw2dvdseu  10256
  Copyright terms: Public domain W3C validator