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

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

Proof of Theorem simplrr
StepHypRef Expression
1 simpr 107 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antlr 466 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:  rmob  2877  isotr  5483  riota5f  5519  tfrexlem  5978  fopwdom  6340  fisbth  6370  fin0  6372  fin0or  6373  diffisn  6380  fientri3  6383  ordiso2  6414  addcmpblnq  6522  mulcmpblnq  6523  ordpipqqs  6529  ltexnqq  6563  addcmpblnq0  6598  mulcmpblnq0  6599  prmu  6633  addlocpr  6691  prmuloc  6721  prmuloc2  6722  ltaddpr  6752  ltexprlemopl  6756  ltexprlemopu  6758  ltexprlemloc  6762  ltexprlemrl  6765  ltexprlemru  6767  addcanprleml  6769  addcanprlemu  6770  aptiprleml  6794  aptiprlemu  6795  ltmprr  6797  cauappcvgprlemloc  6807  archrecpr  6819  caucvgprlemloc  6830  caucvgprprlemloc  6858  caucvgprprlemexbt  6861  addcmpblnr  6881  mulcmpblnrlemg  6882  mulcmpblnr  6883  ltsrprg  6889  mulgt0sr  6919  caucvgsrlemgt1  6936  axmulcl  6999  axarch  7022  axcaucvglemres  7030  readdcan  7213  cnegexlem1  7248  negeu  7264  add20  7542  apreap  7651  cru  7666  apsym  7670  apcotr  7671  apadd1  7672  apneg  7675  mulext1  7676  divdivdivap  7763  ltmul12a  7900  lemul12a  7902  lt2mul2div  7919  ledivdiv  7930  lediv12a  7934  qapne  8670  ixxss12  8875  ioodisj  8961  fz0fzelfz0  9085  qtri3or  9199  qbtwnzlemstep  9204  qbtwnzlemex  9206  qbtwnz  9207  rebtwn2zlemstep  9208  rebtwn2z  9210  qbtwnre  9212  btwnzge0  9249  expivallem  9420  mulexpzap  9459  leexp1a  9474  expnbnd  9539  cjap  9733  cvg1nlemres  9811  rsqrmo  9853  abs3lem  9937  cau3lem  9940  climcau  10096  addmodlteqALT  10170  pw2dvdslemn  10232  pw2dvdseu  10235  qdencn  10490
  Copyright terms: Public domain W3C validator