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

Theorem simprrr 500
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 107 . 2  |-  ( ( ch  /\  th )  ->  th )
21ad2antll 468 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  th )
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:  fliftfun  5464  grpridd  5725  tfrlemisucaccv  5970  addcmpblnq  6523  mulcmpblnq  6524  ordpipqqs  6530  nqnq0pi  6594  addcmpblnq0  6599  mulcmpblnq0  6600  addnq0mo  6603  mulnq0mo  6604  prarloclemcalc  6658  prarloc  6659  nqprl  6707  mullocpr  6727  distrlem4prl  6740  distrlem4pru  6741  ltprordil  6745  ltexprlemlol  6758  ltexprlemopu  6759  ltexprlemupu  6760  ltexprlemru  6768  cauappcvgprlemopl  6802  cauappcvgprlem2  6816  caucvgprlemopl  6825  caucvgprlem2  6836  caucvgprprlemexbt  6862  caucvgprprlem2  6866  addcmpblnr  6882  mulcmpblnrlemg  6883  mulcmpblnr  6884  prsrlem1  6885  addsrmo  6886  mulsrmo  6887  ltsrprg  6890  axmulcl  7000  recriota  7022  ltmul1  7657  divdivdivap  7764  divsubdivap  7779  ledivdiv  7931  lediv12a  7935  qbtwnz  9208  qbtwnre  9213  ioom  9217  iseqcaopr  9406  leexp2r  9474  recvguniq  9822  rsqrmo  9854  pw2dvdseu  10256  oddpwdclemndvds  10259
  Copyright terms: Public domain W3C validator