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  1063  simp2lr  1067  simp3lr  1071  bilukdc  1407  dcun  3560  ifnefals  3603  intab  3903  exmid01  4231  exmidundif  4239  exmidundifim  4240  frirrg  4385  reg2exmidlema  4570  imadiflem  5337  fvco4  5633  fvmptt  5653  fcoconst  5733  f1imass  5821  fcof1  5830  fliftfun  5843  riotass2  5904  ovmpodxf  6048  dftpos4  6321  tfrlem1  6366  tfrlem3ag  6367  tfrlemibacc  6384  tfrlemibfn  6386  tfrlemi1  6390  tfrlemi14d  6391  tfr1onlem3ag  6395  tfr1onlembacc  6400  tfr1onlembfn  6402  tfr1onlemaccex  6406  tfrcllembacc  6413  tfrcllembfn  6415  tfrcllemaccex  6419  frecabcl  6457  nntr2  6561  dcdifsnid  6562  nnm00  6588  ecopovsymg  6693  ecopoverg  6695  th3qlem1  6696  mapss  6750  f1imaen2g  6852  pw2f1odclem  6895  xpen  6906  xpmapenlem  6910  phpm  6926  fidifsnen  6931  dif1enen  6941  fiunsnnn  6942  fin0  6946  fin0or  6947  findcard2d  6952  findcard2sd  6953  diffifi  6955  isinfinf  6958  tridc  6960  fimax2gtrilemstep  6961  fimax2gtri  6962  en2eqpr  6968  onunsnss  6978  unsnfidcex  6981  unsnfidcel  6982  undifdcss  6984  unfiin  6987  fisseneq  6995  ssfirab  6997  f1finf1o  7013  fidcenumlemrks  7019  fidcenumlemrk  7020  fidcenumlemr  7021  fidcenum  7022  suplub2ti  7067  supisolem  7074  ordiso2  7101  djudom  7159  omp1eomlem  7160  difinfsnlem  7165  difinfinf  7167  ctm  7175  ctssdclemn0  7176  enumct  7181  nnnninfeq  7194  nnnninfeq2  7195  nninfisol  7199  enomnilem  7204  finomni  7206  exmidomni  7208  fodju0  7213  ismkvnex  7221  enmkvlem  7227  enwomnilem  7235  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidaclem  7275  exmidontriimlem1  7288  exmidontriimlem2  7289  exmidontriimlem3  7290  exmidontriimlem4  7291  exmidontriim  7292  netap  7321  exmidapne  7327  dfplpq2  7421  dfmpq2  7422  mulpipqqs  7440  nqpi  7445  distrnqg  7454  prarloclemarch  7485  enq0tr  7501  nqnq0pi  7505  nq0nn  7509  nnnq0lem1  7513  prarloclemup  7562  prarloclem3  7564  prarloclemcalc  7569  genplt2i  7577  addnqprllem  7594  addnqprulem  7595  appdivnq  7630  distrlem1prl  7649  distrlem1pru  7650  ltaddpr  7664  ltexprlemlol  7669  ltexprlemupu  7671  ltexprlemdisj  7673  addcanprleml  7681  ltaprlem  7685  addextpr  7688  recexprlemopu  7694  recexprlemdisj  7697  recexprlem1ssl  7700  aptiprleml  7706  cauappcvgprlemm  7712  cauappcvgprlemopl  7713  cauappcvgprlemlol  7714  cauappcvgprlemopu  7715  cauappcvgprlemdisj  7718  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemopu  7738  caucvgprlemladdfu  7744  caucvgprprlemml  7761  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemopu  7766  caucvgprprlemexbt  7773  suplocexprlemru  7786  suplocexprlemloc  7788  suplocexprlemub  7790  suplocexprlemlub  7791  prsrlem1  7809  recexgt0sr  7840  mulgt0sr  7845  archsr  7849  caucvgsrlemcau  7860  caucvgsrlemoffcau  7865  caucvgsrlemoffres  7867  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  addcnsr  7901  mulcnsr  7902  mulcnsrec  7910  axmulcom  7938  nntopi  7961  axcaucvglemcau  7965  axcaucvglemres  7966  axpre-suploclemres  7968  axpre-suploc  7969  mpomulf  8016  axsuploc  8099  ltntri  8154  cnegexlem2  8202  cnegexlem3  8203  addsub4  8269  le2add  8471  lt2add  8472  lt2sub  8487  le2sub  8488  rereim  8613  apreim  8630  mulreim  8631  apcotr  8634  apadd1  8635  addext  8637  mulext1  8639  mulext  8641  apti  8649  aptap  8677  receuap  8696  rec11rap  8738  divdivdivap  8740  divadddivap  8754  divsubdivap  8755  rerecclap  8757  recgt0  8877  prodgt0gt0  8878  prodgt0  8879  prodge0  8881  lemulge11  8893  lt2mul2div  8906  ltrec  8910  lerec  8911  ltrec1  8915  lediv2a  8922  mulle0r  8971  sup3exmid  8984  zdiv  9414  eluzuzle  9609  supinfneg  9669  infsupneg  9670  infregelbex  9672  xrltso  9871  xnn0dcle  9877  xnn0letri  9878  npnflt  9890  nmnfgt  9893  z2ge  9901  xaddf  9919  xaddval  9920  xpncan  9946  xleadd1a  9948  xltadd1  9951  xaddge0  9953  xle2add  9954  xleaddadd  9962  ixxss1  9979  ixxss2  9980  elico2  10012  iccsupr  10041  fzass4  10137  fzrev  10159  fz0fzelfz0  10202  fzocatel  10275  elfzomelpfzo  10307  zsupcllemstep  10319  exbtwnzlemstep  10337  rebtwn2zlemstep  10342  qbtwnxr  10347  xqltnle  10357  apbtwnz  10364  btwnzge0  10390  modqid  10441  modqcyc  10451  modqcyc2  10452  modqaddabs  10454  modqaddmod  10455  mulqaddmodid  10456  modqmuladd  10458  modqltm1p1mod  10468  modqsubmod  10474  modqsubmodmod  10475  modaddmodlo  10480  modqmulmod  10481  modqmulmodr  10482  modqsubdir  10485  addmodlteq  10490  nninfinf  10535  iseqf1olemab  10594  iseqf1olemmo  10597  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  seqf1oglem1  10611  seqf1oglem2  10612  seqf1og  10613  exp3val  10633  expcl2lemap  10643  expap0  10661  expnegzap  10665  expmul  10676  leexp1a  10686  qsqeqor  10742  expnbnd  10755  nn0ltexp2  10801  nn0opth2  10816  facndiv  10831  faclbnd  10833  bcval5  10855  bcpasc  10858  hashennnuni  10871  hashunlem  10896  hashunsng  10899  hashprg  10900  fiprsshashgt1  10909  hashxp  10918  fimaxq  10919  zfz1isolemiso  10931  zfz1isolem1  10932  seq3coll  10934  iswrdiz  10942  wrdnval  10965  shftlem  10981  shftfvalg  10983  shftfval  10986  2shfti  10996  caucvgrelemrec  11144  caucvgrelemcau  11145  caucvgre  11146  cvg1nlemcau  11149  cvg1nlemres  11150  resqrexlemcalc3  11181  resqrexlemcvg  11184  resqrexlemglsq  11187  resqrexlemga  11188  sqrtsq  11209  leabs  11239  absexpzap  11245  abslt  11253  absle  11254  abssubap0  11255  caubnd2  11282  icodiamlt  11345  maxleim  11370  maxabslemval  11373  maxleastlt  11380  rexico  11386  zmaxcl  11389  fimaxre2  11392  minmax  11395  xrmaxleim  11409  xrmaxiflemcl  11410  xrmaxifle  11411  xrmaxiflemlub  11413  xrmaxiflemval  11415  xrmaxleastlt  11421  xrmaxltsup  11423  xrmaxadd  11426  xrminmax  11430  xrbdtri  11441  climuni  11458  climshftlemg  11467  iserex  11504  climcau  11512  climrecvg1n  11513  climcvg1nlem  11514  sumeq2  11524  summodclem3  11545  zsumdc  11549  isumss  11556  fisumss  11557  sumsnf  11574  fsumconst  11619  modfsummod  11623  fsum00  11627  fsumabs  11630  fsumrelem  11636  fsumiun  11642  isumsplit  11656  divcnv  11662  geo2sum  11679  geoisumr  11683  cvgratz  11697  ntrivcvgap  11713  prodeq2  11722  prodmodclem2  11742  prodmodc  11743  zproddc  11744  fprodmul  11756  prodsnf  11757  fprodcl2lem  11770  fprodconst  11785  fprodap0  11786  fprodrec  11794  fprodap0f  11801  fprodle  11805  fprodmodd  11806  tanaddap  11904  zdvdsdc  11977  dvds2ln  11989  fsumdvds  12007  dvdsle  12009  dvdsext  12020  divalglemeunn  12086  divalglemex  12087  divalglemeuneg  12088  bitsfzo  12119  dvdsbnd  12123  gcdsupex  12124  gcdsupcl  12125  dvdslegcd  12131  bezoutlemnewy  12163  bezoutlemstep  12164  bezoutlemmain  12165  bezoutlemzz  12169  bezoutlembz  12171  bezoutlembi  12172  bezoutlemle  12175  dfgcd3  12177  bezout  12178  dfgcd2  12181  dvdsmulgcd  12192  bezoutr  12199  uzwodc  12204  nninfctlemfo  12207  lcmval  12231  lcmcllem  12235  lcmneg  12242  ncoprmgcdne1b  12257  isprm2lem  12284  prmind2  12288  dvdsnprmd  12293  isprm5  12310  prmdvdsexp  12316  sqrt2irr  12330  oddpwdclemxy  12337  oddpwdclemdc  12341  nonsq  12375  pceu  12464  pcmul  12470  pc2dvds  12499  pcz  12501  pcprmpw2  12502  dvdsprmpweqle  12506  pcfac  12519  qexpz  12521  prmpwdvds  12524  1arith  12536  mul4sq  12563  4sqexercise2  12568  4sqlemsdc  12569  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemhom  12632  ennnfonelemfun  12634  ennnfonelemf1  12635  ennnfonelemim  12641  exmidunben  12643  ctiunctlemfo  12656  omiunct  12661  ssnnctlemct  12663  isstruct2r  12689  ismgm  13000  issgrp  13046  sgrppropd  13056  sgrpidmndm  13061  mndpropd  13081  issubmnd  13083  resmhm2b  13121  gsumwmhm  13130  isgrpinv  13186  grplmulf1o  13206  dfgrp3mlem  13230  grplactcnv  13234  mhmid  13245  mhmmnd  13246  ghmgrp  13248  mulgval  13252  mulgfng  13254  mulgnnp1  13260  mulgnn0dir  13282  mulgneg2  13286  mhmmulg  13293  grpissubg  13324  isnsg  13332  isnsg3  13337  nmzsubg  13340  ghmmhmb  13384  ghmpreima  13396  ghmnsgpreima  13399  ghmf1  13403  ghmf1o  13405  conjghm  13406  conjnmz  13409  conjnmzb  13410  ghmcmn  13457  gsumfzconst  13471  issrg  13521  srglmhm  13549  srgrmhm  13550  isring  13556  ringadd2  13583  ringlghm  13617  ringrghm  13618  oppr1g  13638  reldvdsrsrg  13648  dvdsrvald  13649  dvdsrd  13650  dvdsrex  13654  dvdsrmul1  13658  unitgrp  13672  rhmopp  13732  subrgintm  13799  subrgpropd  13809  isdomn  13825  lmodprop2d  13904  lssvacl  13921  lssvsubcl  13922  lssvscl  13931  lsslss  13937  lss1d  13939  lsspropdg  13987  expghmap  14163  mulgghm2  14164  znunit  14215  znrrg  14216  opnssneib  14392  restbasg  14404  restopn2  14419  iscnp4  14454  cnss2  14463  cnconst2  14469  cnptopresti  14474  cnptoprest2  14476  neitx  14504  uptx  14510  txrest  14512  txdis1cn  14514  xmetres2  14615  xblss2ps  14640  blhalf  14644  blssps  14663  blss  14664  blssexps  14665  blssex  14666  blin2  14668  metequiv2  14732  bdmetval  14736  metcnp3  14747  metcnp  14748  metcn  14750  metcnpi  14751  metcnpi2  14752  txmetcnp  14754  txmetcn  14755  qtopbas  14758  tgqioo  14791  mpomulcn  14802  fsumcncntop  14803  elcncf2  14810  mulcncflem  14843  mulcncf  14844  suplociccreex  14860  limcdifap  14898  cnplimcim  14903  cnplimccntop  14906  limccnpcntop  14911  dvcj  14945  dvmptfsum  14961  dveflem  14962  ply1termlem  14978  plyaddlem1  14983  plymullem1  14984  plycolemc  14994  plycjlemc  14996  plyrecj  14999  dvply1  15001  reeff1olem  15007  eflt  15011  sin0pilem1  15017  ptolemy  15060  coseq0q4123  15070  coseq0negpitopi  15072  cos02pilt1  15087  cos11  15089  ioocosf1o  15090  rpcxpmul2  15149  cxplt  15152  cxple  15153  cxplt3  15156  apcxp2  15175  rprelogbmul  15191  rprelogbdiv  15193  dvdsppwf1o  15225  perfect  15237  lgsval  15245  lgsfcl2  15247  lgscllem  15248  lgsval2lem  15251  lgsdir2lem4  15272  lgsdir2lem5  15273  lgsdir2  15274  lgsne0  15279  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  2sqlem6  15361  2sqlem10  15366  pwle2  15643  pwf1oexmid  15644  subctctexmid  15645  pw1nct  15647  peano4nninf  15650  nninfalllem1  15652  nninfall  15653  nninfsellemeq  15658  nninfsellemqall  15659  sbthom  15670  refeq  15672  isomninnlem  15674  trilpolemeq1  15684  trilpolemlt1  15685  trirec0  15688  apdiff  15692  iswomninnlem  15693  ismkvnnlem  15696  redcwlpolemeq1  15698  ltlenmkv  15714