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

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

Proof of Theorem simprrr
StepHypRef Expression
1 simpr 103 . 2  |-  ( ( ch  /\  th )  ->  th )
21ad2antll 460 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  fliftfun  5436  grpridd  5697  tfrlemisucaccv  5939  addcmpblnq  6465  mulcmpblnq  6466  ordpipqqs  6472  nqnq0pi  6536  addcmpblnq0  6541  mulcmpblnq0  6542  addnq0mo  6545  mulnq0mo  6546  prarloclemcalc  6600  prarloc  6601  nqprl  6649  mullocpr  6669  distrlem4prl  6682  distrlem4pru  6683  ltprordil  6687  ltexprlemlol  6700  ltexprlemopu  6701  ltexprlemupu  6702  ltexprlemru  6710  cauappcvgprlemopl  6744  cauappcvgprlem2  6758  caucvgprlemopl  6767  caucvgprlem2  6778  caucvgprprlemexbt  6804  caucvgprprlem2  6808  addcmpblnr  6824  mulcmpblnrlemg  6825  mulcmpblnr  6826  prsrlem1  6827  addsrmo  6828  mulsrmo  6829  ltsrprg  6832  axmulcl  6942  recriota  6964  ltmul1  7583  divdivdivap  7689  divsubdivap  7704  ledivdiv  7856  lediv12a  7860  qbtwnz  9106  qbtwnre  9111  iseqcaopr  9242  leexp2r  9308  recvguniq  9593  rsqrmo  9625
  Copyright terms: Public domain W3C validator