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

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

Proof of Theorem simprrl
StepHypRef Expression
1 simpl 106 . 2  |-  ( ( ch  /\  th )  ->  ch )
21ad2antll 468 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  ch )
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:  dn1dc  878  imain  5008  grpridd  5724  tfrlemisucaccv  5969  tfrexlem  5978  eroveu  6227  addcmpblnq  6522  mulcmpblnq  6523  ordpipqqs  6529  nqnq0pi  6593  addcmpblnq0  6598  mulcmpblnq0  6599  prarloclemcalc  6657  prarloc  6658  nqpru  6707  mullocpr  6726  distrlem4prl  6739  distrlem4pru  6740  ltprordil  6744  ltexprlemm  6755  ltexprlemopu  6758  ltexprlemupu  6759  ltexprlemru  6767  cauappcvgprlemopl  6801  cauappcvgprlem2  6815  caucvgprlemopl  6824  caucvgprlem2  6835  caucvgprprlemexbt  6861  caucvgprprlem2  6865  addcmpblnr  6881  mulcmpblnrlemg  6882  mulcmpblnr  6883  prsrlem1  6884  ltsrprg  6889  axmulcl  6999  ltmul1  7656  divdivdivap  7763  divmuleqap  7767  divsubdivap  7778  lt2mul2div  7919  ledivdiv  7930  lediv12a  7934  ssfzo12bi  9182  qbtwnz  9207  qbtwnre  9212  ioom  9216  iseqcaopr  9405  leexp2r  9473  recvguniq  9821  rsqrmo  9853  pw2dvdseu  10235  oddpwdclemdvds  10237
  Copyright terms: Public domain W3C validator