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  906  imain  5096  grpridd  5841  tfrlemisucaccv  6090  tfrexlem  6099  tfr1onlemsucaccv  6106  tfrcllemsucaccv  6119  eroveu  6381  addcmpblnq  6924  mulcmpblnq  6925  ordpipqqs  6931  nqnq0pi  6995  addcmpblnq0  7000  mulcmpblnq0  7001  prarloclemcalc  7059  prarloc  7060  nqpru  7109  mullocpr  7128  distrlem4prl  7141  distrlem4pru  7142  ltprordil  7146  ltexprlemm  7157  ltexprlemopu  7160  ltexprlemupu  7161  ltexprlemru  7169  cauappcvgprlemopl  7203  cauappcvgprlem2  7217  caucvgprlemopl  7226  caucvgprlem2  7237  caucvgprprlemexbt  7263  caucvgprprlem2  7267  addcmpblnr  7283  mulcmpblnrlemg  7284  mulcmpblnr  7285  prsrlem1  7286  ltsrprg  7291  axmulcl  7401  ltmul1  8067  divdivdivap  8178  divmuleqap  8182  divsubdivap  8193  lt2mul2div  8338  ledivdiv  8349  lediv12a  8353  ssfzo12bi  9632  exbtwnz  9658  qbtwnre  9664  ioom  9668  iseqcaopr  9908  leexp2r  10005  hashunlem  10208  recvguniq  10424  rsqrmo  10456  fsum2dlemstep  10824  expcnvre  10893  bezout  11274  qredeu  11353  pw2dvdseu  11420  oddpwdclemdvds  11422
  Copyright terms: Public domain W3C validator