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  1085  simp2lr  1089  simp3lr  1093  bilukdc  1438  dcun  3601  ifnefals  3647  intab  3952  exmid01  4282  exmidundif  4290  exmidundifim  4291  frirrg  4441  reg2exmidlema  4626  imadiflem  5400  fvco4  5708  fvmptt  5728  fcoconst  5808  funopsn  5819  f1imass  5904  fcof1  5913  fliftfun  5926  riotass2  5989  ovmpodxf  6136  dftpos4  6415  tfrlem1  6460  tfrlem3ag  6461  tfrlemibacc  6478  tfrlemibfn  6480  tfrlemi1  6484  tfrlemi14d  6485  tfr1onlem3ag  6489  tfr1onlembacc  6494  tfr1onlembfn  6496  tfr1onlemaccex  6500  tfrcllembacc  6507  tfrcllembfn  6509  tfrcllemaccex  6513  frecabcl  6551  nntr2  6657  dcdifsnid  6658  nnm00  6684  ecopovsymg  6789  ecopoverg  6791  th3qlem1  6792  mapss  6846  f1imaen2g  6953  pw2f1odclem  7003  xpen  7014  xpmapenlem  7018  phpm  7035  fidifsnen  7040  dif1enen  7050  fiunsnnn  7051  fin0  7055  fin0or  7056  findcard2d  7061  findcard2sd  7062  diffifi  7064  isinfinf  7067  tridc  7070  fimax2gtrilemstep  7071  fimax2gtri  7072  en2eqpr  7080  onunsnss  7090  unsnfidcex  7093  unsnfidcel  7094  undifdcss  7096  unfiin  7099  fisseneq  7107  ssfirab  7109  f1finf1o  7125  fidcenumlemrks  7131  fidcenumlemrk  7132  fidcenumlemr  7133  fidcenum  7134  suplub2ti  7179  supisolem  7186  ordiso2  7213  djudom  7271  omp1eomlem  7272  difinfsnlem  7277  difinfinf  7279  ctm  7287  ctssdclemn0  7288  enumct  7293  nnnninfeq  7306  nnnninfeq2  7307  nninfisol  7311  enomnilem  7316  finomni  7318  exmidomni  7320  fodju0  7325  ismkvnex  7333  enmkvlem  7339  enwomnilem  7347  pr2cv1  7379  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidaclem  7401  exmidontriimlem1  7414  exmidontriimlem2  7415  exmidontriimlem3  7416  exmidontriimlem4  7417  exmidontriim  7418  netap  7451  exmidapne  7457  dfplpq2  7552  dfmpq2  7553  mulpipqqs  7571  nqpi  7576  distrnqg  7585  prarloclemarch  7616  enq0tr  7632  nqnq0pi  7636  nq0nn  7640  nnnq0lem1  7644  prarloclemup  7693  prarloclem3  7695  prarloclemcalc  7700  genplt2i  7708  addnqprllem  7725  addnqprulem  7726  appdivnq  7761  distrlem1prl  7780  distrlem1pru  7781  ltaddpr  7795  ltexprlemlol  7800  ltexprlemupu  7802  ltexprlemdisj  7804  addcanprleml  7812  ltaprlem  7816  addextpr  7819  recexprlemopu  7825  recexprlemdisj  7828  recexprlem1ssl  7831  aptiprleml  7837  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemopu  7846  cauappcvgprlemdisj  7849  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemopu  7869  caucvgprlemladdfu  7875  caucvgprprlemml  7892  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemexbt  7904  suplocexprlemru  7917  suplocexprlemloc  7919  suplocexprlemub  7921  suplocexprlemlub  7922  prsrlem1  7940  recexgt0sr  7971  mulgt0sr  7976  archsr  7980  caucvgsrlemcau  7991  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  addcnsr  8032  mulcnsr  8033  mulcnsrec  8041  axmulcom  8069  nntopi  8092  axcaucvglemcau  8096  axcaucvglemres  8097  axpre-suploclemres  8099  axpre-suploc  8100  mpomulf  8147  axsuploc  8230  ltntri  8285  cnegexlem2  8333  cnegexlem3  8334  addsub4  8400  le2add  8602  lt2add  8603  lt2sub  8618  le2sub  8619  rereim  8744  apreim  8761  mulreim  8762  apcotr  8765  apadd1  8766  addext  8768  mulext1  8770  mulext  8772  apti  8780  aptap  8808  receuap  8827  rec11rap  8869  divdivdivap  8871  divadddivap  8885  divsubdivap  8886  rerecclap  8888  recgt0  9008  prodgt0gt0  9009  prodgt0  9010  prodge0  9012  lemulge11  9024  lt2mul2div  9037  ltrec  9041  lerec  9042  ltrec1  9046  lediv2a  9053  mulle0r  9102  sup3exmid  9115  zdiv  9546  eluzuzle  9742  supinfneg  9802  infsupneg  9803  infregelbex  9805  xrltso  10004  xnn0dcle  10010  xnn0letri  10011  npnflt  10023  nmnfgt  10026  z2ge  10034  xaddf  10052  xaddval  10053  xpncan  10079  xleadd1a  10081  xltadd1  10084  xaddge0  10086  xle2add  10087  xleaddadd  10095  ixxss1  10112  ixxss2  10113  elico2  10145  iccsupr  10174  fzass4  10270  fzrev  10292  fz0fzelfz0  10335  fzocatel  10417  elfzomelpfzo  10449  zsupcllemstep  10461  exbtwnzlemstep  10479  rebtwn2zlemstep  10484  qbtwnxr  10489  xqltnle  10499  apbtwnz  10506  btwnzge0  10532  modqid  10583  modqcyc  10593  modqcyc2  10594  modqaddabs  10596  modqaddmod  10597  mulqaddmodid  10598  modqmuladd  10600  modqltm1p1mod  10610  modqsubmod  10616  modqsubmodmod  10617  modaddmodlo  10622  modqmulmod  10623  modqmulmodr  10624  modqsubdir  10627  addmodlteq  10632  nninfinf  10677  iseqf1olemab  10736  iseqf1olemmo  10739  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  seqf1oglem1  10753  seqf1oglem2  10754  seqf1og  10755  exp3val  10775  expcl2lemap  10785  expap0  10803  expnegzap  10807  expmul  10818  leexp1a  10828  qsqeqor  10884  expnbnd  10897  nn0ltexp2  10943  nn0opth2  10958  facndiv  10973  faclbnd  10975  bcval5  10997  bcpasc  11000  hashennnuni  11013  hashunlem  11038  hashunsng  11042  hashprg  11043  fiprsshashgt1  11052  hashxp  11061  fimaxq  11062  zfz1isolemiso  11074  zfz1isolem1  11075  seq3coll  11077  iswrdiz  11091  wrdnval  11115  ccatlen  11143  ccatvalfn  11149  ccatsymb  11150  ccatalpha  11161  swrdclg  11197  swrdsb0eq  11212  pfxwrdsymbg  11237  wrdind  11269  wrd2ind  11270  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatin12  11280  pfxccat3  11281  swrdccat  11282  shftlem  11342  shftfvalg  11344  shftfval  11347  2shfti  11357  caucvgrelemrec  11505  caucvgrelemcau  11506  caucvgre  11507  cvg1nlemcau  11510  cvg1nlemres  11511  resqrexlemcalc3  11542  resqrexlemcvg  11545  resqrexlemglsq  11548  resqrexlemga  11549  sqrtsq  11570  leabs  11600  absexpzap  11606  abslt  11614  absle  11615  abssubap0  11616  caubnd2  11643  icodiamlt  11706  maxleim  11731  maxabslemval  11734  maxleastlt  11741  rexico  11747  zmaxcl  11750  fimaxre2  11753  minmax  11756  xrmaxleim  11770  xrmaxiflemcl  11771  xrmaxifle  11772  xrmaxiflemlub  11774  xrmaxiflemval  11776  xrmaxleastlt  11782  xrmaxltsup  11784  xrmaxadd  11787  xrminmax  11791  xrbdtri  11802  climuni  11819  climshftlemg  11828  iserex  11865  climcau  11873  climrecvg1n  11874  climcvg1nlem  11875  sumeq2  11885  summodclem3  11906  zsumdc  11910  isumss  11917  fisumss  11918  sumsnf  11935  fsumconst  11980  modfsummod  11984  fsum00  11988  fsumabs  11991  fsumrelem  11997  fsumiun  12003  isumsplit  12017  divcnv  12023  geo2sum  12040  geoisumr  12044  cvgratz  12058  ntrivcvgap  12074  prodeq2  12083  prodmodclem2  12103  prodmodc  12104  zproddc  12105  fprodmul  12117  prodsnf  12118  fprodcl2lem  12131  fprodconst  12146  fprodap0  12147  fprodrec  12155  fprodap0f  12162  fprodle  12166  fprodmodd  12167  tanaddap  12265  zdvdsdc  12338  dvds2ln  12350  fsumdvds  12368  dvdsle  12370  dvdsext  12381  divalglemeunn  12447  divalglemex  12448  divalglemeuneg  12449  bitsfzo  12481  bitsmod  12482  bitsinv1lem  12487  bitsinv1  12488  dvdsbnd  12492  gcdsupex  12493  gcdsupcl  12494  dvdslegcd  12500  bezoutlemnewy  12532  bezoutlemstep  12533  bezoutlemmain  12534  bezoutlemzz  12538  bezoutlembz  12540  bezoutlembi  12541  bezoutlemle  12544  dfgcd3  12546  bezout  12547  dfgcd2  12550  dvdsmulgcd  12561  bezoutr  12568  uzwodc  12573  nninfctlemfo  12576  lcmval  12600  lcmcllem  12604  lcmneg  12611  ncoprmgcdne1b  12626  isprm2lem  12653  prmind2  12657  dvdsnprmd  12662  isprm5  12679  prmdvdsexp  12685  sqrt2irr  12699  oddpwdclemxy  12706  oddpwdclemdc  12710  nonsq  12744  pceu  12833  pcmul  12839  pc2dvds  12868  pcz  12870  pcprmpw2  12871  dvdsprmpweqle  12875  pcfac  12888  qexpz  12890  prmpwdvds  12893  1arith  12905  mul4sq  12932  4sqexercise2  12937  4sqlemsdc  12938  ennnfonelemkh  12998  ennnfonelemhf1o  12999  ennnfonelemhom  13001  ennnfonelemfun  13003  ennnfonelemf1  13004  ennnfonelemim  13010  exmidunben  13012  ctiunctlemfo  13025  omiunct  13030  ssnnctlemct  13032  isstruct2r  13058  prdsval  13321  ismgm  13405  issgrp  13451  sgrppropd  13461  sgrpidmndm  13468  mndpropd  13488  issubmnd  13490  prdsidlem  13495  resmhm2b  13537  gsumwmhm  13546  isgrpinv  13602  grplmulf1o  13622  dfgrp3mlem  13646  grplactcnv  13650  pwssub  13661  mhmid  13667  mhmmnd  13668  ghmgrp  13670  mulgval  13674  mulgfng  13676  mulgnnp1  13682  mulgnn0dir  13704  mulgneg2  13708  mhmmulg  13715  grpissubg  13746  isnsg  13754  isnsg3  13759  nmzsubg  13762  ghmmhmb  13806  ghmpreima  13818  ghmnsgpreima  13821  ghmf1  13825  ghmf1o  13827  conjghm  13828  conjnmz  13831  conjnmzb  13832  ghmcmn  13879  gsumfzconst  13893  issrg  13943  srglmhm  13971  srgrmhm  13972  isring  13978  ringadd2  14005  ringlghm  14039  ringrghm  14040  oppr1g  14060  dvdsrvald  14072  dvdsrd  14073  dvdsrex  14077  dvdsrmul1  14081  unitgrp  14095  rhmopp  14155  subrgintm  14222  subrgpropd  14232  isdomn  14248  lmodprop2d  14327  lssvacl  14344  lssvsubcl  14345  lssvscl  14354  lsslss  14360  lss1d  14362  lsspropdg  14410  expghmap  14586  mulgghm2  14587  znunit  14638  znrrg  14639  mplvalcoe  14669  mplsubgfilemcl  14678  mplsubgfileminv  14679  mplsubgfi  14680  opnssneib  14845  restbasg  14857  restopn2  14872  iscnp4  14907  cnss2  14916  cnconst2  14922  cnptopresti  14927  cnptoprest2  14929  neitx  14957  uptx  14963  txrest  14965  txdis1cn  14967  xmetres2  15068  xblss2ps  15093  blhalf  15097  blssps  15116  blss  15117  blssexps  15118  blssex  15119  blin2  15121  metequiv2  15185  bdmetval  15189  metcnp3  15200  metcnp  15201  metcn  15203  metcnpi  15204  metcnpi2  15205  txmetcnp  15207  txmetcn  15208  qtopbas  15211  tgqioo  15244  mpomulcn  15255  fsumcncntop  15256  elcncf2  15263  mulcncflem  15296  mulcncf  15297  suplociccreex  15313  limcdifap  15351  cnplimcim  15356  cnplimccntop  15359  limccnpcntop  15364  dvcj  15398  dvmptfsum  15414  dveflem  15415  ply1termlem  15431  plyaddlem1  15436  plymullem1  15437  plycolemc  15447  plycjlemc  15449  plyrecj  15452  dvply1  15454  reeff1olem  15460  eflt  15464  sin0pilem1  15470  ptolemy  15513  coseq0q4123  15523  coseq0negpitopi  15525  cos02pilt1  15540  cos11  15542  ioocosf1o  15543  rpcxpmul2  15602  cxplt  15605  cxple  15606  cxplt3  15609  apcxp2  15628  rprelogbmul  15644  rprelogbdiv  15646  dvdsppwf1o  15678  perfect  15690  lgsval  15698  lgsfcl2  15700  lgscllem  15701  lgsval2lem  15704  lgsdir2lem4  15725  lgsdir2lem5  15726  lgsdir2  15727  lgsne0  15732  gausslemma2dlem1a  15752  gausslemma2dlem1f1o  15754  2sqlem6  15814  2sqlem10  15819  umgrnloopv  15929  umgrvad2edg  16024  wlkvtxiedg  16086  wlkvtxiedgg  16087  upgredginwlk  16097  upgriswlkdc  16101  clwwlkccatlem  16137  pw1ndom3  16413  2omap  16418  pw1map  16420  pwle2  16423  pwf1oexmid  16424  subctctexmid  16425  pw1nct  16428  peano4nninf  16432  nninfalllem1  16434  nninfall  16435  nninfsellemeq  16440  nninfsellemqall  16441  nnnninfex  16448  nninfnfiinf  16449  sbthom  16454  refeq  16456  isomninnlem  16458  trilpolemeq1  16468  trilpolemlt1  16469  trirec0  16472  apdiff  16476  iswomninnlem  16477  ismkvnnlem  16480  redcwlpolemeq1  16482  ltlenmkv  16498