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

Theorem simplr 490
Description: Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)
Assertion
Ref Expression
simplr  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )

Proof of Theorem simplr
StepHypRef Expression
1 id 19 . 2  |-  ( ps 
->  ps )
21ad2antlr 466 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
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:  simp1lr  979  simp2lr  983  simp3lr  987  bilukdc  1303  intab  3672  frirrg  4115  reg2exmidlema  4287  imadiflem  5006  fvmptt  5290  fcoconst  5362  f1imass  5441  fcof1  5451  fliftfun  5464  riotass2  5522  ovmpt2dxf  5654  dftpos4  5909  tfrlem1  5954  tfrlem3ag  5955  tfrlemibacc  5971  tfrlemibfn  5973  tfrlemi1  5977  tfrlemi14d  5978  nndifsnid  6111  nnm00  6133  ecopovsymg  6236  ecopoverg  6238  th3qlem1  6239  f1imaen2g  6304  phpm  6358  fidifsnen  6362  fidifsnid  6363  fiunsnnn  6369  fin0  6373  fin0or  6374  findcard2d  6379  findcard2sd  6380  diffifi  6382  onunsnss  6386  supisolem  6412  ordiso2  6415  dfplpq2  6510  dfmpq2  6511  mulpipqqs  6529  nqpi  6534  distrnqg  6543  prarloclemarch  6574  enq0tr  6590  nqnq0pi  6594  nq0nn  6598  nnnq0lem1  6602  prarloclemup  6651  prarloclem3  6653  prarloclemcalc  6658  genplt2i  6666  addnqprllem  6683  addnqprulem  6684  appdivnq  6719  distrlem1prl  6738  distrlem1pru  6739  ltaddpr  6753  ltexprlemlol  6758  ltexprlemupu  6760  ltexprlemdisj  6762  addcanprleml  6770  ltaprlem  6774  addextpr  6777  recexprlemopu  6783  recexprlemdisj  6786  recexprlem1ssl  6789  aptiprleml  6795  cauappcvgprlemm  6801  cauappcvgprlemopl  6802  cauappcvgprlemlol  6803  cauappcvgprlemopu  6804  cauappcvgprlemdisj  6807  cauappcvgprlemladdfu  6810  cauappcvgprlemladdfl  6811  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  caucvgprlemm  6824  caucvgprlemopl  6825  caucvgprlemlol  6826  caucvgprlemopu  6827  caucvgprlemladdfu  6833  caucvgprprlemml  6850  caucvgprprlemopl  6853  caucvgprprlemlol  6854  caucvgprprlemopu  6855  caucvgprprlemexbt  6862  prsrlem1  6885  recexgt0sr  6916  mulgt0sr  6920  archsr  6924  caucvgsrlemcau  6935  caucvgsrlemoffcau  6940  caucvgsrlemoffres  6942  addcnsr  6968  mulcnsr  6969  mulcnsrec  6977  axmulcom  7003  nntopi  7026  axcaucvglemcau  7030  axcaucvglemres  7031  cnegexlem2  7250  cnegexlem3  7251  addsub4  7317  le2add  7513  lt2add  7514  lt2sub  7529  le2sub  7530  rereim  7651  apreim  7668  mulreim  7669  apcotr  7672  apadd1  7673  addext  7675  mulext1  7677  mulext  7679  apti  7687  receuap  7724  rec11rap  7762  divdivdivap  7764  divadddivap  7778  divsubdivap  7779  rerecclap  7781  recgt0  7891  prodgt0gt0  7892  prodgt0  7893  prodge0  7895  lemulge11  7907  lt2mul2div  7920  ltrec  7924  lerec  7925  ltrec1  7929  lediv2a  7936  mulle0r  7985  zdiv  8386  eluzuzle  8577  xrltso  8818  z2ge  8840  ixxss1  8874  ixxss2  8875  elico2  8907  iccsupr  8936  fzass4  9027  fzrev  9048  fz0fzelfz0  9086  fzocatel  9157  elfzomelpfzo  9189  rebtwn2zlemstep  9209  qbtwnxr  9214  btwnzge0  9250  modqid  9299  modqcyc  9309  modqcyc2  9310  modqaddabs  9312  modqaddmod  9313  mulqaddmodid  9314  modqmuladd  9316  modqltm1p1mod  9326  modqsubmod  9332  modqsubmodmod  9333  modaddmodlo  9338  modqmulmod  9339  modqmulmodr  9340  modqsubdir  9343  addmodlteq  9348  expival  9422  expcl2lemap  9432  expap0  9450  expnegzap  9454  expmul  9465  leexp1a  9475  expnbnd  9540  nn0opth2  9592  facndiv  9607  faclbnd  9609  ibcval5  9631  bcpasc  9634  shftlem  9645  shftfvalg  9647  shftfval  9650  2shfti  9660  caucvgrelemrec  9806  caucvgrelemcau  9807  caucvgre  9808  cvg1nlemcau  9811  cvg1nlemres  9812  resqrexlemcalc3  9843  resqrexlemcvg  9846  resqrexlemglsq  9849  resqrexlemga  9850  sqrtsq  9871  leabs  9901  absexpzap  9907  abslt  9915  absle  9916  abssubap0  9917  caubnd2  9944  icodiamlt  10007  climuni  10045  climshftlemg  10054  iiserex  10090  climcau  10097  climrecvg1n  10098  climcvg1nlem  10099  dvds2ln  10140  dvdsle  10156  dvdsext  10167  divalglemeunn  10233  divalglemex  10234  divalglemeuneg  10235  sqrt2irr  10251  oddpwdclemxy  10257  oddpwdclemdc  10261
  Copyright terms: Public domain W3C validator