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

Theorem simplr 497
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 473 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
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:  simp1lr  1005  simp2lr  1009  simp3lr  1013  bilukdc  1330  intab  3700  exmid01  4006  exmidundif  4009  frirrg  4151  reg2exmidlema  4323  imadiflem  5058  fvco4  5339  fvmptt  5357  fcoconst  5431  f1imass  5514  fcof1  5523  fliftfun  5536  riotass2  5595  ovmpt2dxf  5727  dftpos4  5982  tfrlem1  6027  tfrlem3ag  6028  tfrlemibacc  6045  tfrlemibfn  6047  tfrlemi1  6051  tfrlemi14d  6052  tfr1onlem3ag  6056  tfr1onlembacc  6061  tfr1onlembfn  6063  tfr1onlemaccex  6067  tfrcllembacc  6074  tfrcllembfn  6076  tfrcllemaccex  6080  frecabcl  6118  dcdifsnid  6217  nnm00  6240  ecopovsymg  6343  ecopoverg  6345  th3qlem1  6346  mapss  6400  f1imaen2g  6462  xpen  6513  xpmapenlem  6517  phpm  6533  fidifsnen  6538  dif1enen  6548  fiunsnnn  6549  fin0  6553  fin0or  6554  findcard2d  6559  findcard2sd  6560  diffifi  6562  isinfinf  6565  tridc  6567  fimax2gtrilemstep  6568  fimax2gtri  6569  en2eqpr  6575  onunsnss  6579  unsnfidcex  6582  unsnfidcel  6583  undifdcss  6585  unfiin  6588  fisseneq  6592  ssfirab  6593  f1finf1o  6605  suplub2ti  6640  supisolem  6647  ordiso2  6672  djudom  6731  enomnilem  6738  finomni  6740  exmidomni  6742  fodjuomnilem0  6746  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  dfplpq2  6857  dfmpq2  6858  mulpipqqs  6876  nqpi  6881  distrnqg  6890  prarloclemarch  6921  enq0tr  6937  nqnq0pi  6941  nq0nn  6945  nnnq0lem1  6949  prarloclemup  6998  prarloclem3  7000  prarloclemcalc  7005  genplt2i  7013  addnqprllem  7030  addnqprulem  7031  appdivnq  7066  distrlem1prl  7085  distrlem1pru  7086  ltaddpr  7100  ltexprlemlol  7105  ltexprlemupu  7107  ltexprlemdisj  7109  addcanprleml  7117  ltaprlem  7121  addextpr  7124  recexprlemopu  7130  recexprlemdisj  7133  recexprlem1ssl  7136  aptiprleml  7142  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemlol  7150  cauappcvgprlemopu  7151  cauappcvgprlemdisj  7154  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemopu  7174  caucvgprlemladdfu  7180  caucvgprprlemml  7197  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemopu  7202  caucvgprprlemexbt  7209  prsrlem1  7232  recexgt0sr  7263  mulgt0sr  7267  archsr  7271  caucvgsrlemcau  7282  caucvgsrlemoffcau  7287  caucvgsrlemoffres  7289  addcnsr  7315  mulcnsr  7316  mulcnsrec  7324  axmulcom  7350  nntopi  7373  axcaucvglemcau  7377  axcaucvglemres  7378  cnegexlem2  7602  cnegexlem3  7603  addsub4  7669  le2add  7866  lt2add  7867  lt2sub  7882  le2sub  7883  rereim  8004  apreim  8021  mulreim  8022  apcotr  8025  apadd1  8026  addext  8028  mulext1  8030  mulext  8032  apti  8040  receuap  8077  rec11rap  8117  divdivdivap  8119  divadddivap  8133  divsubdivap  8134  rerecclap  8136  recgt0  8246  prodgt0gt0  8247  prodgt0  8248  prodge0  8250  lemulge11  8262  lt2mul2div  8275  ltrec  8279  lerec  8280  ltrec1  8284  lediv2a  8291  mulle0r  8340  zdiv  8767  eluzuzle  8959  supinfneg  9015  infsupneg  9016  xrltso  9198  z2ge  9220  ixxss1  9254  ixxss2  9255  elico2  9287  iccsupr  9316  fzass4  9407  fzrev  9428  fz0fzelfz0  9466  fzocatel  9538  elfzomelpfzo  9570  exbtwnzlemstep  9587  rebtwn2zlemstep  9592  qbtwnxr  9597  apbtwnz  9609  btwnzge0  9635  modqid  9684  modqcyc  9694  modqcyc2  9695  modqaddabs  9697  modqaddmod  9698  mulqaddmodid  9699  modqmuladd  9701  modqltm1p1mod  9711  modqsubmod  9717  modqsubmodmod  9718  modaddmodlo  9723  modqmulmod  9724  modqmulmodr  9725  modqsubdir  9728  addmodlteq  9733  iseqf1olemab  9823  iseqf1olemmo  9826  iseqf1olemjpcl  9829  iseqf1olemqpcl  9830  expival  9856  expcl2lemap  9866  expap0  9884  expnegzap  9888  expmul  9899  leexp1a  9909  expnbnd  9974  nn0opth2  10029  facndiv  10044  faclbnd  10046  ibcval5  10068  bcpasc  10071  hashennnuni  10084  hashunlem  10109  hashunsng  10112  hashprg  10113  fiprsshashgt1  10122  hashxp  10131  fimaxq  10132  zfz1isolemiso  10141  zfz1isolem1  10142  iseqcoll  10144  shftlem  10147  shftfvalg  10149  shftfval  10152  2shfti  10162  caucvgrelemrec  10308  caucvgrelemcau  10309  caucvgre  10310  cvg1nlemcau  10313  cvg1nlemres  10314  resqrexlemcalc3  10345  resqrexlemcvg  10348  resqrexlemglsq  10351  resqrexlemga  10352  sqrtsq  10373  leabs  10403  absexpzap  10409  abslt  10417  absle  10418  abssubap0  10419  caubnd2  10446  icodiamlt  10509  maxleim  10534  maxabslemval  10537  maxleastlt  10544  rexico  10550  zmaxcl  10552  fimaxre2  10553  minmax  10556  climuni  10576  climshftlemg  10585  iiserex  10621  climcau  10628  climrecvg1n  10629  climcvg1nlem  10630  sumeq2  10640  isummolem3  10661  zisum  10665  isumss  10671  fisumss  10672  zdvdsdc  10699  dvds2ln  10711  dvdsle  10727  dvdsext  10738  divalglemeunn  10803  divalglemex  10804  divalglemeuneg  10805  zsupcllemstep  10823  dvdsbnd  10830  gcdsupex  10831  gcdsupcl  10832  dvdslegcd  10838  bezoutlemnewy  10867  bezoutlemstep  10868  bezoutlemmain  10869  bezoutlemzz  10873  bezoutlembz  10875  bezoutlembi  10876  bezoutlemle  10879  dfgcd3  10881  bezout  10882  dfgcd2  10885  dvdsmulgcd  10896  bezoutr  10903  lcmval  10927  lcmcllem  10931  lcmneg  10938  ncoprmgcdne1b  10953  isprm2lem  10980  prmind2  10984  dvdsnprmd  10989  prmdvdsexp  11009  sqrt2irr  11023  oddpwdclemxy  11029  oddpwdclemdc  11033  nonsq  11067  peano4nninf  11341  nninfalllemn  11343  nninfalllem1  11344  nninfall  11345  nninfsellemeq  11351  nninfsellemqall  11352
  Copyright terms: Public domain W3C validator