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

Theorem simprrl 506
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 107 . 2  |-  ( ( ch  /\  th )  ->  ch )
21ad2antll 475 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  dn1dc  902  imain  5049  grpridd  5776  tfrlemisucaccv  6022  tfrexlem  6031  tfr1onlemsucaccv  6038  tfrcllemsucaccv  6051  eroveu  6313  addcmpblnq  6829  mulcmpblnq  6830  ordpipqqs  6836  nqnq0pi  6900  addcmpblnq0  6905  mulcmpblnq0  6906  prarloclemcalc  6964  prarloc  6965  nqpru  7014  mullocpr  7033  distrlem4prl  7046  distrlem4pru  7047  ltprordil  7051  ltexprlemm  7062  ltexprlemopu  7065  ltexprlemupu  7066  ltexprlemru  7074  cauappcvgprlemopl  7108  cauappcvgprlem2  7122  caucvgprlemopl  7131  caucvgprlem2  7142  caucvgprprlemexbt  7168  caucvgprprlem2  7172  addcmpblnr  7188  mulcmpblnrlemg  7189  mulcmpblnr  7190  prsrlem1  7191  ltsrprg  7196  axmulcl  7306  ltmul1  7969  divdivdivap  8078  divmuleqap  8082  divsubdivap  8093  lt2mul2div  8234  ledivdiv  8245  lediv12a  8249  ssfzo12bi  9525  exbtwnz  9551  qbtwnre  9557  ioom  9561  iseqcaopr  9777  leexp2r  9846  hashunlem  10047  recvguniq  10255  rsqrmo  10287  bezout  10780  qredeu  10859  pw2dvdseu  10926  oddpwdclemdvds  10928
  Copyright terms: Public domain W3C validator