Theorem simplr 528

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  1064  simp2lr  1068  simp3lr  1072  bilukdc  1416  dcun  3574  ifnefals  3619  intab  3923  exmid01  4253  exmidundif  4261  exmidundifim  4262  frirrg  4410  reg2exmidlema  4595  imadiflem  5367  fvco4  5669  fvmptt  5689  fcoconst  5769  funopsn  5780  f1imass  5861  fcof1  5870  fliftfun  5883  riotass2  5944  ovmpodxf  6089  dftpos4  6367  tfrlem1  6412  tfrlem3ag  6413  tfrlemibacc  6430  tfrlemibfn  6432  tfrlemi1  6436  tfrlemi14d  6437  tfr1onlem3ag  6441  tfr1onlembacc  6446  tfr1onlembfn  6448  tfr1onlemaccex  6452  tfrcllembacc  6459  tfrcllembfn  6461  tfrcllemaccex  6465  frecabcl  6503  nntr2  6607  dcdifsnid  6608  nnm00  6634  ecopovsymg  6739  ecopoverg  6741  th3qlem1  6742  mapss  6796  f1imaen2g  6903  pw2f1odclem  6951  xpen  6962  xpmapenlem  6966  phpm  6983  fidifsnen  6988  dif1enen  6998  fiunsnnn  6999  fin0  7003  fin0or  7004  findcard2d  7009  findcard2sd  7010  diffifi  7012  isinfinf  7015  tridc  7017  fimax2gtrilemstep  7018  fimax2gtri  7019  en2eqpr  7025  onunsnss  7035  unsnfidcex  7038  unsnfidcel  7039  undifdcss  7041  unfiin  7044  fisseneq  7052  ssfirab  7054  f1finf1o  7070  fidcenumlemrks  7076  fidcenumlemrk  7077  fidcenumlemr  7078  fidcenum  7079  suplub2ti  7124  supisolem  7131  ordiso2  7158  djudom  7216  omp1eomlem  7217  difinfsnlem  7222  difinfinf  7224  ctm  7232  ctssdclemn0  7233  enumct  7238  nnnninfeq  7251  nnnninfeq2  7252  nninfisol  7256  enomnilem  7261  finomni  7263  exmidomni  7265  fodju0  7270  ismkvnex  7278  enmkvlem  7284  enwomnilem  7292  pr2cv1  7324  exmidfodomrlemr  7336  exmidfodomrlemrALT  7337  exmidaclem  7346  exmidontriimlem1  7359  exmidontriimlem2  7360  exmidontriimlem3  7361  exmidontriimlem4  7362  exmidontriim  7363  netap  7396  exmidapne  7402  dfplpq2  7497  dfmpq2  7498  mulpipqqs  7516  nqpi  7521  distrnqg  7530  prarloclemarch  7561  enq0tr  7577  nqnq0pi  7581  nq0nn  7585  nnnq0lem1  7589  prarloclemup  7638  prarloclem3  7640  prarloclemcalc  7645  genplt2i  7653  addnqprllem  7670  addnqprulem  7671  appdivnq  7706  distrlem1prl  7725  distrlem1pru  7726  ltaddpr  7740  ltexprlemlol  7745  ltexprlemupu  7747  ltexprlemdisj  7749  addcanprleml  7757  ltaprlem  7761  addextpr  7764  recexprlemopu  7770  recexprlemdisj  7773  recexprlem1ssl  7776  aptiprleml  7782  cauappcvgprlemm  7788  cauappcvgprlemopl  7789  cauappcvgprlemlol  7790  cauappcvgprlemopu  7791  cauappcvgprlemdisj  7794  cauappcvgprlemladdfu  7797  cauappcvgprlemladdfl  7798  cauappcvgprlemladdru  7799  cauappcvgprlemladdrl  7800  caucvgprlemm  7811  caucvgprlemopl  7812  caucvgprlemlol  7813  caucvgprlemopu  7814  caucvgprlemladdfu  7820  caucvgprprlemml  7837  caucvgprprlemopl  7840  caucvgprprlemlol  7841  caucvgprprlemopu  7842  caucvgprprlemexbt  7849  suplocexprlemru  7862  suplocexprlemloc  7864  suplocexprlemub  7866  suplocexprlemlub  7867  prsrlem1  7885  recexgt0sr  7916  mulgt0sr  7921  archsr  7925  caucvgsrlemcau  7936  caucvgsrlemoffcau  7941  caucvgsrlemoffres  7943  suplocsrlemb  7949  suplocsrlempr  7950  suplocsrlem  7951  addcnsr  7977  mulcnsr  7978  mulcnsrec  7986  axmulcom  8014  nntopi  8037  axcaucvglemcau  8041  axcaucvglemres  8042  axpre-suploclemres  8044  axpre-suploc  8045  mpomulf  8092  axsuploc  8175  ltntri  8230  cnegexlem2  8278  cnegexlem3  8279  addsub4  8345  le2add  8547  lt2add  8548  lt2sub  8563  le2sub  8564  rereim  8689  apreim  8706  mulreim  8707  apcotr  8710  apadd1  8711  addext  8713  mulext1  8715  mulext  8717  apti  8725  aptap  8753  receuap  8772  rec11rap  8814  divdivdivap  8816  divadddivap  8830  divsubdivap  8831  rerecclap  8833  recgt0  8953  prodgt0gt0  8954  prodgt0  8955  prodge0  8957  lemulge11  8969  lt2mul2div  8982  ltrec  8986  lerec  8987  ltrec1  8991  lediv2a  8998  mulle0r  9047  sup3exmid  9060  zdiv  9491  eluzuzle  9686  supinfneg  9746  infsupneg  9747  infregelbex  9749  xrltso  9948  xnn0dcle  9954  xnn0letri  9955  npnflt  9967  nmnfgt  9970  z2ge  9978  xaddf  9996  xaddval  9997  xpncan  10023  xleadd1a  10025  xltadd1  10028  xaddge0  10030  xle2add  10031  xleaddadd  10039  ixxss1  10056  ixxss2  10057  elico2  10089  iccsupr  10118  fzass4  10214  fzrev  10236  fz0fzelfz0  10279  fzocatel  10360  elfzomelpfzo  10392  zsupcllemstep  10404  exbtwnzlemstep  10422  rebtwn2zlemstep  10427  qbtwnxr  10432  xqltnle  10442  apbtwnz  10449  btwnzge0  10475  modqid  10526  modqcyc  10536  modqcyc2  10537  modqaddabs  10539  modqaddmod  10540  mulqaddmodid  10541  modqmuladd  10543  modqltm1p1mod  10553  modqsubmod  10559  modqsubmodmod  10560  modaddmodlo  10565  modqmulmod  10566  modqmulmodr  10567  modqsubdir  10570  addmodlteq  10575  nninfinf  10620  iseqf1olemab  10679  iseqf1olemmo  10682  iseqf1olemjpcl  10685  iseqf1olemqpcl  10686  seqf1oglem1  10696  seqf1oglem2  10697  seqf1og  10698  exp3val  10718  expcl2lemap  10728  expap0  10746  expnegzap  10750  expmul  10761  leexp1a  10771  qsqeqor  10827  expnbnd  10840  nn0ltexp2  10886  nn0opth2  10901  facndiv  10916  faclbnd  10918  bcval5  10940  bcpasc  10943  hashennnuni  10956  hashunlem  10981  hashunsng  10984  hashprg  10985  fiprsshashgt1  10994  hashxp  11003  fimaxq  11004  zfz1isolemiso  11016  zfz1isolem1  11017  seq3coll  11019  iswrdiz  11033  wrdnval  11056  ccatlen  11084  ccatvalfn  11090  ccatsymb  11091  swrdclg  11136  swrdsb0eq  11151  pfxwrdsymbg  11176  wrdind  11208  wrd2ind  11209  shftlem  11212  shftfvalg  11214  shftfval  11217  2shfti  11227  caucvgrelemrec  11375  caucvgrelemcau  11376  caucvgre  11377  cvg1nlemcau  11380  cvg1nlemres  11381  resqrexlemcalc3  11412  resqrexlemcvg  11415  resqrexlemglsq  11418  resqrexlemga  11419  sqrtsq  11440  leabs  11470  absexpzap  11476  abslt  11484  absle  11485  abssubap0  11486  caubnd2  11513  icodiamlt  11576  maxleim  11601  maxabslemval  11604  maxleastlt  11611  rexico  11617  zmaxcl  11620  fimaxre2  11623  minmax  11626  xrmaxleim  11640  xrmaxiflemcl  11641  xrmaxifle  11642  xrmaxiflemlub  11644  xrmaxiflemval  11646  xrmaxleastlt  11652  xrmaxltsup  11654  xrmaxadd  11657  xrminmax  11661  xrbdtri  11672  climuni  11689  climshftlemg  11698  iserex  11735  climcau  11743  climrecvg1n  11744  climcvg1nlem  11745  sumeq2  11755  summodclem3  11776  zsumdc  11780  isumss  11787  fisumss  11788  sumsnf  11805  fsumconst  11850  modfsummod  11854  fsum00  11858  fsumabs  11861  fsumrelem  11867  fsumiun  11873  isumsplit  11887  divcnv  11893  geo2sum  11910  geoisumr  11914  cvgratz  11928  ntrivcvgap  11944  prodeq2  11953  prodmodclem2  11973  prodmodc  11974  zproddc  11975  fprodmul  11987  prodsnf  11988  fprodcl2lem  12001  fprodconst  12016  fprodap0  12017  fprodrec  12025  fprodap0f  12032  fprodle  12036  fprodmodd  12037  tanaddap  12135  zdvdsdc  12208  dvds2ln  12220  fsumdvds  12238  dvdsle  12240  dvdsext  12251  divalglemeunn  12317  divalglemex  12318  divalglemeuneg  12319  bitsfzo  12351  bitsmod  12352  bitsinv1lem  12357  bitsinv1  12358  dvdsbnd  12362  gcdsupex  12363  gcdsupcl  12364  dvdslegcd  12370  bezoutlemnewy  12402  bezoutlemstep  12403  bezoutlemmain  12404  bezoutlemzz  12408  bezoutlembz  12410  bezoutlembi  12411  bezoutlemle  12414  dfgcd3  12416  bezout  12417  dfgcd2  12420  dvdsmulgcd  12431  bezoutr  12438  uzwodc  12443  nninfctlemfo  12446  lcmval  12470  lcmcllem  12474  lcmneg  12481  ncoprmgcdne1b  12496  isprm2lem  12523  prmind2  12527  dvdsnprmd  12532  isprm5  12549  prmdvdsexp  12555  sqrt2irr  12569  oddpwdclemxy  12576  oddpwdclemdc  12580  nonsq  12614  pceu  12703  pcmul  12709  pc2dvds  12738  pcz  12740  pcprmpw2  12741  dvdsprmpweqle  12745  pcfac  12758  qexpz  12760  prmpwdvds  12763  1arith  12775  mul4sq  12802  4sqexercise2  12807  4sqlemsdc  12808  ennnfonelemkh  12868  ennnfonelemhf1o  12869  ennnfonelemhom  12871  ennnfonelemfun  12873  ennnfonelemf1  12874  ennnfonelemim  12880  exmidunben  12882  ctiunctlemfo  12895  omiunct  12900  ssnnctlemct  12902  isstruct2r  12928  prdsval  13190  ismgm  13274  issgrp  13320  sgrppropd  13330  sgrpidmndm  13337  mndpropd  13357  issubmnd  13359  prdsidlem  13364  resmhm2b  13406  gsumwmhm  13415  isgrpinv  13471  grplmulf1o  13491  dfgrp3mlem  13515  grplactcnv  13519  pwssub  13530  mhmid  13536  mhmmnd  13537  ghmgrp  13539  mulgval  13543  mulgfng  13545  mulgnnp1  13551  mulgnn0dir  13573  mulgneg2  13577  mhmmulg  13584  grpissubg  13615  isnsg  13623  isnsg3  13628  nmzsubg  13631  ghmmhmb  13675  ghmpreima  13687  ghmnsgpreima  13690  ghmf1  13694  ghmf1o  13696  conjghm  13697  conjnmz  13700  conjnmzb  13701  ghmcmn  13748  gsumfzconst  13762  issrg  13812  srglmhm  13840  srgrmhm  13841  isring  13847  ringadd2  13874  ringlghm  13908  ringrghm  13909  oppr1g  13929  reldvdsrsrg  13939  dvdsrvald  13940  dvdsrd  13941  dvdsrex  13945  dvdsrmul1  13949  unitgrp  13963  rhmopp  14023  subrgintm  14090  subrgpropd  14100  isdomn  14116  lmodprop2d  14195  lssvacl  14212  lssvsubcl  14213  lssvscl  14222  lsslss  14228  lss1d  14230  lsspropdg  14278  expghmap  14454  mulgghm2  14455  znunit  14506  znrrg  14507  mplvalcoe  14537  mplsubgfilemcl  14546  mplsubgfileminv  14547  mplsubgfi  14548  opnssneib  14713  restbasg  14725  restopn2  14740  iscnp4  14775  cnss2  14784  cnconst2  14790  cnptopresti  14795  cnptoprest2  14797  neitx  14825  uptx  14831  txrest  14833  txdis1cn  14835  xmetres2  14936  xblss2ps  14961  blhalf  14965  blssps  14984  blss  14985  blssexps  14986  blssex  14987  blin2  14989  metequiv2  15053  bdmetval  15057  metcnp3  15068  metcnp  15069  metcn  15071  metcnpi  15072  metcnpi2  15073  txmetcnp  15075  txmetcn  15076  qtopbas  15079  tgqioo  15112  mpomulcn  15123  fsumcncntop  15124  elcncf2  15131  mulcncflem  15164  mulcncf  15165  suplociccreex  15181  limcdifap  15219  cnplimcim  15224  cnplimccntop  15227  limccnpcntop  15232  dvcj  15266  dvmptfsum  15282  dveflem  15283  ply1termlem  15299  plyaddlem1  15304  plymullem1  15305  plycolemc  15315  plycjlemc  15317  plyrecj  15320  dvply1  15322  reeff1olem  15328  eflt  15332  sin0pilem1  15338  ptolemy  15381  coseq0q4123  15391  coseq0negpitopi  15393  cos02pilt1  15408  cos11  15410  ioocosf1o  15411  rpcxpmul2  15470  cxplt  15473  cxple  15474  cxplt3  15477  apcxp2  15496  rprelogbmul  15512  rprelogbdiv  15514  dvdsppwf1o  15546  perfect  15558  lgsval  15566  lgsfcl2  15568  lgscllem  15569  lgsval2lem  15572  lgsdir2lem4  15593  lgsdir2lem5  15594  lgsdir2  15595  lgsne0  15600  gausslemma2dlem1a  15620  gausslemma2dlem1f1o  15622  2sqlem6  15682  2sqlem10  15687  umgrnloopvv  15795  2omap  16102  pw1map  16104  pwle2  16107  pwf1oexmid  16108  subctctexmid  16109  pw1nct  16112  peano4nninf  16115  nninfalllem1  16117  nninfall  16118  nninfsellemeq  16123  nninfsellemqall  16124  nnnninfex  16131  nninfnfiinf  16132  sbthom  16137  refeq  16139  isomninnlem  16141  trilpolemeq1  16151  trilpolemlt1  16152  trirec0  16155  apdiff  16159  iswomninnlem  16160  ismkvnnlem  16163  redcwlpolemeq1  16165  ltlenmkv  16181