Theorem simplr 529

Description: Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)

Assertion

Ref	Expression
simplr	|- ( ( ( ph /\ ps ) /\ ch ) -> ps )

Proof of Theorem simplr

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ps -> ps )
2	1	ad2antlr 489	1 |- ( ( ( ph /\ ps ) /\ ch ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simp1lr  1088  simp2lr  1092  simp3lr  1096  bilukdc  1441  dcun  3606  ifnefals  3654  intab  3962  exmid01  4294  exmidundif  4302  exmidundifim  4303  frirrg  4453  reg2exmidlema  4638  imadiflem  5416  fvco4  5727  fvmptt  5747  fcoconst  5826  funopsn  5838  f1imass  5925  fcof1  5934  fliftfun  5947  riotass2  6010  ovmpodxf  6157  fsuppeq  6425  fsuppeqg  6426  suppssdc  6438  suppssfvg  6441  dftpos4  6472  tfrlem1  6517  tfrlem3ag  6518  tfrlemibacc  6535  tfrlemibfn  6537  tfrlemi1  6541  tfrlemi14d  6542  tfr1onlem3ag  6546  tfr1onlembacc  6551  tfr1onlembfn  6553  tfr1onlemaccex  6557  tfrcllembacc  6564  tfrcllembfn  6566  tfrcllemaccex  6570  frecabcl  6608  nntr2  6714  dcdifsnid  6715  nnm00  6741  ecopovsymg  6846  ecopoverg  6848  th3qlem1  6849  mapss  6903  f1imaen2g  7010  pw2f1odclem  7063  xpen  7074  xpmapenlem  7078  phpm  7095  fidifsnen  7100  dif1enen  7112  fiunsnnn  7113  fin0  7117  fin0or  7118  findcard2d  7123  findcard2sd  7124  diffifi  7126  isinfinf  7129  tridc  7132  fimax2gtrilemstep  7133  fimax2gtri  7134  en2eqpr  7142  onunsnss  7152  unsnfidcex  7155  unsnfidcel  7156  undifdcss  7158  unfiin  7161  fisseneq  7170  ssfirab  7172  f1finf1o  7189  fidcenumlemrks  7195  fidcenumlemrk  7196  fidcenumlemr  7197  fidcenum  7198  suplub2ti  7243  supisolem  7250  ordiso2  7277  djudom  7335  omp1eomlem  7336  difinfsnlem  7341  difinfinf  7343  ctm  7351  ctssdclemn0  7352  enumct  7357  nnnninfeq  7370  nnnninfeq2  7371  nninfisol  7375  enomnilem  7380  finomni  7382  exmidomni  7384  fodju0  7389  ismkvnex  7397  enmkvlem  7403  enwomnilem  7411  pr2cv1  7443  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  exmidaclem  7466  exmidontriimlem1  7479  exmidontriimlem2  7480  exmidontriimlem3  7481  exmidontriimlem4  7482  exmidontriim  7483  netap  7516  exmidapne  7522  dfplpq2  7617  dfmpq2  7618  mulpipqqs  7636  nqpi  7641  distrnqg  7650  prarloclemarch  7681  enq0tr  7697  nqnq0pi  7701  nq0nn  7705  nnnq0lem1  7709  prarloclemup  7758  prarloclem3  7760  prarloclemcalc  7765  genplt2i  7773  addnqprllem  7790  addnqprulem  7791  appdivnq  7826  distrlem1prl  7845  distrlem1pru  7846  ltaddpr  7860  ltexprlemlol  7865  ltexprlemupu  7867  ltexprlemdisj  7869  addcanprleml  7877  ltaprlem  7881  addextpr  7884  recexprlemopu  7890  recexprlemdisj  7893  recexprlem1ssl  7896  aptiprleml  7902  cauappcvgprlemm  7908  cauappcvgprlemopl  7909  cauappcvgprlemlol  7910  cauappcvgprlemopu  7911  cauappcvgprlemdisj  7914  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemm  7931  caucvgprlemopl  7932  caucvgprlemlol  7933  caucvgprlemopu  7934  caucvgprlemladdfu  7940  caucvgprprlemml  7957  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemopu  7962  caucvgprprlemexbt  7969  suplocexprlemru  7982  suplocexprlemloc  7984  suplocexprlemub  7986  suplocexprlemlub  7987  prsrlem1  8005  recexgt0sr  8036  mulgt0sr  8041  archsr  8045  caucvgsrlemcau  8056  caucvgsrlemoffcau  8061  caucvgsrlemoffres  8063  suplocsrlemb  8069  suplocsrlempr  8070  suplocsrlem  8071  addcnsr  8097  mulcnsr  8098  mulcnsrec  8106  axmulcom  8134  nntopi  8157  axcaucvglemcau  8161  axcaucvglemres  8162  axpre-suploclemres  8164  axpre-suploc  8165  mpomulf  8212  axsuploc  8294  ltntri  8349  cnegexlem2  8397  cnegexlem3  8398  addsub4  8464  le2add  8666  lt2add  8667  lt2sub  8682  le2sub  8683  rereim  8808  apreim  8825  mulreim  8826  apcotr  8829  apadd1  8830  addext  8832  mulext1  8834  mulext  8836  apti  8844  aptap  8872  receuap  8891  rec11rap  8933  divdivdivap  8935  divadddivap  8949  divsubdivap  8950  rerecclap  8952  recgt0  9072  prodgt0gt0  9073  prodgt0  9074  prodge0  9076  lemulge11  9088  lt2mul2div  9101  ltrec  9105  lerec  9106  ltrec1  9110  lediv2a  9117  mulle0r  9166  sup3exmid  9179  zdiv  9612  eluzuzle  9808  supinfneg  9873  infsupneg  9874  infregelbex  9876  xrltso  10075  xnn0dcle  10081  xnn0letri  10082  npnflt  10094  nmnfgt  10097  z2ge  10105  xaddf  10123  xaddval  10124  xpncan  10150  xleadd1a  10152  xltadd1  10155  xaddge0  10157  xle2add  10158  xleaddadd  10166  ixxss1  10183  ixxss2  10184  elico2  10216  iccsupr  10245  fzass4  10342  fzrev  10364  fz0fzelfz0  10407  fzocatel  10490  elfzomelpfzo  10522  zsupcllemstep  10535  exbtwnzlemstep  10553  rebtwn2zlemstep  10558  qbtwnxr  10563  xqltnle  10573  apbtwnz  10580  btwnzge0  10606  modqid  10657  modqcyc  10667  modqcyc2  10668  modqaddabs  10670  modqaddmod  10671  mulqaddmodid  10672  modqmuladd  10674  modqltm1p1mod  10684  modqsubmod  10690  modqsubmodmod  10691  modaddmodlo  10696  modqmulmod  10697  modqmulmodr  10698  modqsubdir  10701  addmodlteq  10706  nninfinf  10751  iseqf1olemab  10810  iseqf1olemmo  10813  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  seqf1oglem1  10827  seqf1oglem2  10828  seqf1og  10829  exp3val  10849  expcl2lemap  10859  expap0  10877  expnegzap  10881  expmul  10892  leexp1a  10902  qsqeqor  10958  expnbnd  10971  nn0ltexp2  11017  nn0opth2  11032  facndiv  11047  faclbnd  11049  bcval5  11071  bcpasc  11074  hashennnuni  11087  hashunlem  11113  hashunsng  11117  hashprg  11118  fiprsshashgt1  11127  hashxp  11136  fimaxq  11137  zfz1isolemiso  11149  zfz1isolem1  11150  seq3coll  11152  iswrdiz  11169  wrdnval  11193  ccatlen  11221  ccatvalfn  11227  ccatsymb  11228  ccatalpha  11239  ccat2s1fstg  11274  swrdclg  11280  swrdsb0eq  11295  pfxwrdsymbg  11320  wrdind  11352  wrd2ind  11353  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatin12  11363  pfxccat3  11364  swrdccat  11365  shftlem  11439  shftfvalg  11441  shftfval  11444  2shfti  11454  caucvgrelemrec  11602  caucvgrelemcau  11603  caucvgre  11604  cvg1nlemcau  11607  cvg1nlemres  11608  resqrexlemcalc3  11639  resqrexlemcvg  11642  resqrexlemglsq  11645  resqrexlemga  11646  sqrtsq  11667  leabs  11697  absexpzap  11703  abslt  11711  absle  11712  abssubap0  11713  caubnd2  11740  icodiamlt  11803  maxleim  11828  maxabslemval  11831  maxleastlt  11838  rexico  11844  zmaxcl  11847  fimaxre2  11850  minmax  11853  xrmaxleim  11867  xrmaxiflemcl  11868  xrmaxifle  11869  xrmaxiflemlub  11871  xrmaxiflemval  11873  xrmaxleastlt  11879  xrmaxltsup  11881  xrmaxadd  11884  xrminmax  11888  xrbdtri  11899  climuni  11916  climshftlemg  11925  iserex  11962  climcau  11970  climrecvg1n  11971  climcvg1nlem  11972  sumeq2  11982  summodclem3  12004  zsumdc  12008  isumss  12015  fisumss  12016  sumsnf  12033  fsumconst  12078  modfsummod  12082  fsum00  12086  fsumabs  12089  fsumrelem  12095  fsumiun  12101  isumsplit  12115  divcnv  12121  geo2sum  12138  geoisumr  12142  cvgratz  12156  ntrivcvgap  12172  prodeq2  12181  prodmodclem2  12201  prodmodc  12202  zproddc  12203  fprodmul  12215  prodsnf  12216  fprodcl2lem  12229  fprodconst  12244  fprodap0  12245  fprodrec  12253  fprodap0f  12260  fprodle  12264  fprodmodd  12265  tanaddap  12363  zdvdsdc  12436  dvds2ln  12448  fsumdvds  12466  dvdsle  12468  dvdsext  12479  divalglemeunn  12545  divalglemex  12546  divalglemeuneg  12547  bitsfzo  12579  bitsmod  12580  bitsinv1lem  12585  bitsinv1  12586  dvdsbnd  12590  gcdsupex  12591  gcdsupcl  12592  dvdslegcd  12598  bezoutlemnewy  12630  bezoutlemstep  12631  bezoutlemmain  12632  bezoutlemzz  12636  bezoutlembz  12638  bezoutlembi  12639  bezoutlemle  12642  dfgcd3  12644  bezout  12645  dfgcd2  12648  dvdsmulgcd  12659  bezoutr  12666  uzwodc  12671  nninfctlemfo  12674  lcmval  12698  lcmcllem  12702  lcmneg  12709  ncoprmgcdne1b  12724  isprm2lem  12751  prmind2  12755  dvdsnprmd  12760  isprm5  12777  prmdvdsexp  12783  sqrt2irr  12797  oddpwdclemxy  12804  oddpwdclemdc  12808  nonsq  12842  pceu  12931  pcmul  12937  pc2dvds  12966  pcz  12968  pcprmpw2  12969  dvdsprmpweqle  12973  pcfac  12986  qexpz  12988  prmpwdvds  12991  1arith  13003  mul4sq  13030  4sqexercise2  13035  4sqlemsdc  13036  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemhom  13099  ennnfonelemfun  13101  ennnfonelemf1  13102  ennnfonelemim  13108  exmidunben  13110  ctiunctlemfo  13123  omiunct  13128  ssnnctlemct  13130  isstruct2r  13156  prdsval  13419  ismgm  13503  issgrp  13549  sgrppropd  13559  sgrpidmndm  13566  mndpropd  13586  issubmnd  13588  prdsidlem  13593  resmhm2b  13635  gsumwmhm  13644  isgrpinv  13700  grplmulf1o  13720  dfgrp3mlem  13744  grplactcnv  13748  pwssub  13759  mhmid  13765  mhmmnd  13766  ghmgrp  13768  mulgval  13772  mulgfng  13774  mulgnnp1  13780  mulgnn0dir  13802  mulgneg2  13806  mhmmulg  13813  grpissubg  13844  isnsg  13852  isnsg3  13857  nmzsubg  13860  ghmmhmb  13904  ghmpreima  13916  ghmnsgpreima  13919  ghmf1  13923  ghmf1o  13925  conjghm  13926  conjnmz  13929  conjnmzb  13930  ghmcmn  13977  gsumfzconst  13991  issrg  14042  srglmhm  14070  srgrmhm  14071  isring  14077  ringadd2  14104  ringlghm  14138  ringrghm  14139  oppr1g  14159  dvdsrvald  14171  dvdsrd  14172  dvdsrex  14176  dvdsrmul1  14180  unitgrp  14194  rhmopp  14254  subrgintm  14321  subrgpropd  14331  isdomn  14348  lmodprop2d  14427  lssvacl  14444  lssvsubcl  14445  lssvscl  14454  lsslss  14460  lss1d  14462  lsspropdg  14510  expghmap  14686  mulgghm2  14687  znunit  14738  znrrg  14739  mplvalcoe  14774  mplsubgfilemcl  14783  mplsubgfileminv  14784  mplsubgfi  14785  opnssneib  14950  restbasg  14962  restopn2  14977  iscnp4  15012  cnss2  15021  cnconst2  15027  cnptopresti  15032  cnptoprest2  15034  neitx  15062  uptx  15068  txrest  15070  txdis1cn  15072  xmetres2  15173  xblss2ps  15198  blhalf  15202  blssps  15221  blss  15222  blssexps  15223  blssex  15224  blin2  15226  metequiv2  15290  bdmetval  15294  metcnp3  15305  metcnp  15306  metcn  15308  metcnpi  15309  metcnpi2  15310  txmetcnp  15312  txmetcn  15313  qtopbas  15316  tgqioo  15349  mpomulcn  15360  fsumcncntop  15361  elcncf2  15368  mulcncflem  15401  mulcncf  15402  suplociccreex  15418  limcdifap  15456  cnplimcim  15461  cnplimccntop  15464  limccnpcntop  15469  dvcj  15503  dvmptfsum  15519  dveflem  15520  ply1termlem  15536  plyaddlem1  15541  plymullem1  15542  plycolemc  15552  plycjlemc  15554  plyrecj  15557  dvply1  15559  reeff1olem  15565  eflt  15569  sin0pilem1  15575  ptolemy  15618  coseq0q4123  15628  coseq0negpitopi  15630  cos02pilt1  15645  cos11  15647  ioocosf1o  15648  rpcxpmul2  15707  cxplt  15710  cxple  15711  cxplt3  15714  apcxp2  15733  rprelogbmul  15749  rprelogbdiv  15751  pellexlem3  15776  dvdsppwf1o  15786  perfect  15798  lgsval  15806  lgsfcl2  15808  lgscllem  15809  lgsval2lem  15812  lgsdir2lem4  15833  lgsdir2lem5  15834  lgsdir2  15835  lgsne0  15840  gausslemma2dlem1a  15860  gausslemma2dlem1f1o  15862  2sqlem6  15922  2sqlem10  15927  umgrnloopv  16038  umgrvad2edg  16135  usgr1eop  16169  wlkvtxiedg  16269  wlkvtxiedgg  16270  upgredginwlk  16280  upgriswlkdc  16284  clwwlkccatlem  16324  eupth2lem3lem4fi  16397  pw1ndom3  16693  2omap  16698  pw1map  16700  pwle2  16703  pwf1oexmid  16704  subctctexmid  16705  pw1nct  16708  peano4nninf  16715  nninfalllem1  16717  nninfall  16718  nninfsellemeq  16723  nninfsellemqall  16724  nnnninfex  16731  nninfnfiinf  16732  sbthom  16737  refeq  16739  isomninnlem  16745  trilpolemeq1  16755  trilpolemlt1  16756  trirec0  16759  apdiff  16763  iswomninnlem  16765  ismkvnnlem  16768  redcwlpolemeq1  16770  ltlenmkv  16786  gfsumcl  16799