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

Theorem simprrr 530
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 109 . 2  |-  ( ( ch  /\  th )  ->  th )
21ad2antll 483 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  th )
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:  fliftfun  5759  grpridd  6030  tfrlemisucaccv  6285  tfr1onlemsucaccv  6301  tfrcllemsucaccv  6314  addcmpblnq  7300  mulcmpblnq  7301  ordpipqqs  7307  nqnq0pi  7371  addcmpblnq0  7376  mulcmpblnq0  7377  addnq0mo  7380  mulnq0mo  7381  prarloclemcalc  7435  prarloc  7436  nqprl  7484  mullocpr  7504  distrlem4prl  7517  distrlem4pru  7518  ltprordil  7522  ltexprlemlol  7535  ltexprlemopu  7536  ltexprlemupu  7537  ltexprlemru  7545  cauappcvgprlemopl  7579  cauappcvgprlem2  7593  caucvgprlemopl  7602  caucvgprlem2  7613  caucvgprprlemexbt  7639  caucvgprprlem2  7643  suplocexprlemloc  7654  suplocexprlemub  7656  suplocexprlemlub  7657  addcmpblnr  7672  mulcmpblnrlemg  7673  mulcmpblnr  7674  prsrlem1  7675  addsrmo  7676  mulsrmo  7677  ltsrprg  7680  axmulcl  7799  recriota  7823  ltmul1  8482  divdivdivap  8601  divsubdivap  8616  ledivdiv  8777  lediv12a  8781  exbtwnz  10177  qbtwnre  10183  ioom  10187  seq3caopr  10409  leexp2r  10500  hashunlem  10707  recvguniq  10924  rsqrmo  10956  fsum2dlemstep  11362  expcnvre  11431  fprod2dlemstep  11550  suprzcl2dc  11874  bezout  11930  qredeu  12015  pw2dvdseu  12086  oddpwdclemndvds  12089  pcqmul  12221  pcadd  12257  pockthg  12273  epttop  12648  restbasg  12726  iscnp4  12776  cnptopco  12780  blssps  12985  blss  12986  metequiv2  13054  xmetxpbl  13066  suplociccex  13161  dedekindicc  13169  limcimolemlt  13191
  Copyright terms: Public domain W3C validator