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  3619  ifnefals  3667  intab  3978  exmid01  4311  exmidundif  4319  exmidundifim  4320  frirrg  4471  reg2exmidlema  4656  imadiflem  5435  fvco4  5749  fvmptt  5769  fcoconst  5848  funopsn  5860  f1imass  5947  fcof1  5956  fliftfun  5969  riotass2  6032  ovmpodxf  6179  fsuppeq  6447  fsuppeqg  6448  suppssdc  6460  suppssfvg  6463  dftpos4  6494  tfrlem1  6539  tfrlem3ag  6540  tfrlemibacc  6557  tfrlemibfn  6559  tfrlemi1  6563  tfrlemi14d  6564  tfr1onlem3ag  6568  tfr1onlembacc  6573  tfr1onlembfn  6575  tfr1onlemaccex  6579  tfrcllembacc  6586  tfrcllembfn  6588  tfrcllemaccex  6592  frecabcl  6630  nntr2  6736  dcdifsnid  6737  nnm00  6763  ecopovsymg  6868  ecopoverg  6870  th3qlem1  6871  mapss  6926  f1imaen2g  7033  pw2f1odclem  7087  xpen  7098  xpmapenlem  7102  mapunen  7104  phpm  7120  fidifsnen  7125  dif1enen  7137  fiunsnnn  7138  fin0  7142  fin0or  7143  findcard2d  7148  findcard2sd  7149  diffifi  7151  isinfinf  7154  tridc  7157  fimax2gtrilemstep  7158  fimax2gtri  7159  en2eqpr  7167  onunsnss  7177  unsnfidcex  7180  unsnfidcel  7181  undifdcss  7183  unfiin  7186  fisseneq  7195  ssfirab  7197  f1finf1o  7217  fidcenumlemrks  7223  fidcenumlemrk  7224  fidcenumlemr  7225  fidcenum  7226  ffsuppbi  7253  2omap  7269  suplub2ti  7292  supisolem  7299  ordiso2  7326  djudom  7384  omp1eomlem  7385  difinfsnlem  7390  difinfinf  7392  ctm  7400  ctssdclemn0  7401  enumct  7406  nnnninfeq  7419  nnnninfeq2  7420  nninfisol  7424  enomnilem  7429  finomni  7431  exmidomni  7433  fodju0  7438  ismkvnex  7446  enmkvlem  7452  enwomnilem  7460  pr2cv1  7492  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  exmidaclem  7515  exmidontriimlem1  7528  exmidontriimlem2  7529  exmidontriimlem3  7530  exmidontriimlem4  7531  exmidontriim  7532  netap  7568  exmidapne  7574  dfplpq2  7669  dfmpq2  7670  mulpipqqs  7688  nqpi  7693  distrnqg  7702  prarloclemarch  7733  enq0tr  7749  nqnq0pi  7753  nq0nn  7757  nnnq0lem1  7761  prarloclemup  7810  prarloclem3  7812  prarloclemcalc  7817  genplt2i  7825  addnqprllem  7842  addnqprulem  7843  appdivnq  7878  distrlem1prl  7897  distrlem1pru  7898  ltaddpr  7912  ltexprlemlol  7917  ltexprlemupu  7919  ltexprlemdisj  7921  addcanprleml  7929  ltaprlem  7933  addextpr  7936  recexprlemopu  7942  recexprlemdisj  7945  recexprlem1ssl  7948  aptiprleml  7954  cauappcvgprlemm  7960  cauappcvgprlemopl  7961  cauappcvgprlemlol  7962  cauappcvgprlemopu  7963  cauappcvgprlemdisj  7966  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  caucvgprlemm  7983  caucvgprlemopl  7984  caucvgprlemlol  7985  caucvgprlemopu  7986  caucvgprlemladdfu  7992  caucvgprprlemml  8009  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemopu  8014  caucvgprprlemexbt  8021  suplocexprlemru  8034  suplocexprlemloc  8036  suplocexprlemub  8038  suplocexprlemlub  8039  prsrlem1  8057  recexgt0sr  8088  mulgt0sr  8093  archsr  8097  caucvgsrlemcau  8108  caucvgsrlemoffcau  8113  caucvgsrlemoffres  8115  suplocsrlemb  8121  suplocsrlempr  8122  suplocsrlem  8123  addcnsr  8149  mulcnsr  8150  mulcnsrec  8158  axmulcom  8186  nntopi  8209  axcaucvglemcau  8213  axcaucvglemres  8214  axpre-suploclemres  8216  axpre-suploc  8217  mpomulf  8264  axsuploc  8346  ltntri  8401  cnegexlem2  8449  cnegexlem3  8450  addsub4  8516  le2add  8718  lt2add  8719  lt2sub  8734  le2sub  8735  rereim  8860  apreim  8877  mulreim  8878  apcotr  8881  apadd1  8882  addext  8884  mulext1  8886  mulext  8888  apti  8896  aptap  8924  receuap  8943  rec11rap  8985  divdivdivap  8987  divadddivap  9001  divsubdivap  9002  rerecclap  9004  recgt0  9124  prodgt0gt0  9125  prodgt0  9126  prodge0  9128  lemulge11  9140  lt2mul2div  9153  ltrec  9157  lerec  9158  ltrec1  9162  lediv2a  9169  mulle0r  9218  sup3exmid  9231  zdiv  9666  eluzuzle  9862  supinfneg  9927  infsupneg  9928  infregelbex  9930  xrltso  10129  xnn0dcle  10135  xnn0letri  10136  npnflt  10148  nmnfgt  10151  z2ge  10159  xaddf  10177  xaddval  10178  xpncan  10204  xleadd1a  10206  xltadd1  10209  xaddge0  10211  xle2add  10212  xleaddadd  10220  ixxss1  10237  ixxss2  10238  elico2  10270  iccsupr  10299  fzass4  10396  fzrev  10418  fz0fzelfz0  10461  fzocatel  10544  elfzomelpfzo  10576  zsupcllemstep  10589  exbtwnzlemstep  10607  rebtwn2zlemstep  10612  qbtwnxr  10617  xqltnle  10627  apbtwnz  10634  btwnzge0  10660  modqid  10711  modqcyc  10721  modqcyc2  10722  modqaddabs  10724  modqaddmod  10725  mulqaddmodid  10726  modqmuladd  10728  modqltm1p1mod  10738  modqsubmod  10744  modqsubmodmod  10745  modaddmodlo  10750  modqmulmod  10751  modqmulmodr  10752  modqsubdir  10755  addmodlteq  10760  nninfinf  10805  iseqf1olemab  10864  iseqf1olemmo  10867  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  seqf1oglem1  10881  seqf1oglem2  10882  seqf1og  10883  exp3val  10903  expcl2lemap  10913  expap0  10931  expnegzap  10935  expmul  10946  leexp1a  10956  qsqeqor  11012  expnbnd  11025  nn0ltexp2  11071  nn0opth2  11086  facndiv  11101  faclbnd  11103  bcval5  11125  bcpasc  11128  hashennnuni  11142  hashunlem  11168  hashunsng  11172  hashprg  11173  fiprsshashgt1  11182  hashxp  11191  fimaxq  11194  hashfibc  11207  zfz1isolemiso  11211  zfz1isolem1  11212  seq3coll  11214  iswrdiz  11231  wrdnval  11255  ccatlen  11283  ccatvalfn  11289  ccatsymb  11290  ccatalpha  11301  ccat2s1fstg  11336  swrdclg  11342  swrdsb0eq  11357  pfxwrdsymbg  11382  wrdind  11414  wrd2ind  11415  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12  11425  pfxccat3  11426  swrdccat  11427  shftlem  11501  shftfvalg  11503  shftfval  11506  2shfti  11516  caucvgrelemrec  11664  caucvgrelemcau  11665  caucvgre  11666  cvg1nlemcau  11669  cvg1nlemres  11670  resqrexlemcalc3  11701  resqrexlemcvg  11704  resqrexlemglsq  11707  resqrexlemga  11708  sqrtsq  11729  leabs  11759  absexpzap  11765  abslt  11773  absle  11774  abssubap0  11775  caubnd2  11802  icodiamlt  11865  maxleim  11890  maxabslemval  11893  maxleastlt  11900  rexico  11906  zmaxcl  11909  fimaxre2  11912  minmax  11915  xrmaxleim  11929  xrmaxiflemcl  11930  xrmaxifle  11931  xrmaxiflemlub  11933  xrmaxiflemval  11935  xrmaxleastlt  11941  xrmaxltsup  11943  xrmaxadd  11946  xrminmax  11950  xrbdtri  11961  climuni  11978  climshftlemg  11987  iserex  12024  climcau  12032  climrecvg1n  12033  climcvg1nlem  12034  sumeq2  12044  summodclem3  12066  zsumdc  12070  isumss  12077  fisumss  12078  sumsnf  12095  fsumconst  12140  modfsummod  12144  fsum00  12148  fsumabs  12151  fsumrelem  12157  fsumiun  12163  isumsplit  12177  divcnv  12183  geo2sum  12200  geoisumr  12204  cvgratz  12218  ntrivcvgap  12234  prodeq2  12243  prodmodclem2  12263  prodmodc  12264  zproddc  12265  fprodmul  12277  prodsnf  12278  fprodcl2lem  12291  fprodconst  12306  fprodap0  12307  fprodrec  12315  fprodap0f  12322  fprodle  12326  fprodmodd  12327  tanaddap  12425  zdvdsdc  12498  dvds2ln  12510  fsumdvds  12528  dvdsle  12530  dvdsext  12541  divalglemeunn  12607  divalglemex  12608  divalglemeuneg  12609  bitsfzo  12641  bitsmod  12642  bitsinv1lem  12647  bitsinv1  12648  dvdsbnd  12652  gcdsupex  12653  gcdsupcl  12654  dvdslegcd  12660  bezoutlemnewy  12692  bezoutlemstep  12693  bezoutlemmain  12694  bezoutlemzz  12698  bezoutlembz  12700  bezoutlembi  12701  bezoutlemle  12704  dfgcd3  12706  bezout  12707  dfgcd2  12710  dvdsmulgcd  12721  bezoutr  12728  uzwodc  12733  nninfctlemfo  12736  lcmval  12760  lcmcllem  12764  lcmneg  12771  ncoprmgcdne1b  12786  isprm2lem  12813  prmind2  12817  dvdsnprmd  12822  isprm5  12839  prmdvdsexp  12845  sqrt2irr  12859  oddpwdclemxy  12866  oddpwdclemdc  12870  nonsq  12904  pceu  12993  pcmul  12999  pc2dvds  13028  pcz  13030  pcprmpw2  13031  dvdsprmpweqle  13035  pcfac  13048  qexpz  13050  prmpwdvds  13053  1arith  13065  mul4sq  13092  4sqexercise2  13097  4sqlemsdc  13098  ballotfilem2  13142  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemhom  13166  ennnfonelemfun  13168  ennnfonelemf1  13169  ennnfonelemim  13175  exmidunben  13177  ctiunctlemfo  13190  omiunct  13195  ssnnctlemct  13197  isstruct2r  13223  prdsval  13486  ismgm  13570  issgrp  13616  sgrppropd  13626  sgrpidmndm  13633  mndpropd  13653  issubmnd  13655  prdsidlem  13660  resmhm2b  13702  gsumwmhm  13711  isgrpinv  13767  grplmulf1o  13787  dfgrp3mlem  13811  grplactcnv  13815  pwssub  13826  mhmid  13832  mhmmnd  13833  ghmgrp  13835  mulgval  13839  mulgfng  13841  mulgnnp1  13847  mulgnn0dir  13869  mulgneg2  13873  mhmmulg  13880  grpissubg  13911  isnsg  13919  isnsg3  13924  nmzsubg  13927  ghmmhmb  13971  ghmpreima  13983  ghmnsgpreima  13986  ghmf1  13990  ghmf1o  13992  conjghm  13993  conjnmz  13996  conjnmzb  13997  ghmcmn  14044  gsumfzconst  14058  issrg  14109  srglmhm  14137  srgrmhm  14138  isring  14144  ringadd2  14171  ringlghm  14205  ringrghm  14206  oppr1g  14226  dvdsrvald  14238  dvdsrd  14239  dvdsrex  14243  dvdsrmul1  14247  unitgrp  14261  rhmopp  14321  subrgintm  14388  subrgpropd  14398  isdomn  14415  aprnzr  14433  lmodprop2d  14496  lssvacl  14513  lssvsubcl  14514  lssvscl  14523  lsslss  14529  lss1d  14531  lsspropdg  14579  expghmap  14755  mulgghm2  14756  znunit  14807  znrrg  14808  mplvalcoe  14845  mplsubgfilemcl  14854  mplsubgfileminv  14855  mplsubgfi  14856  opnssneib  15021  restbasg  15033  restopn2  15048  iscnp4  15083  cnss2  15092  cnconst2  15098  cnptopresti  15103  cnptoprest2  15105  neitx  15133  uptx  15139  txrest  15141  txdis1cn  15143  xmetres2  15244  xblss2ps  15269  blhalf  15273  blssps  15292  blss  15293  blssexps  15294  blssex  15295  blin2  15297  metequiv2  15361  bdmetval  15365  metcnp3  15376  metcnp  15377  metcn  15379  metcnpi  15380  metcnpi2  15381  txmetcnp  15383  txmetcn  15384  qtopbas  15387  tgqioo  15420  mpomulcn  15431  fsumcncntop  15432  elcncf2  15439  mulcncflem  15472  mulcncf  15473  suplociccreex  15489  limcdifap  15527  cnplimcim  15532  cnplimccntop  15535  limccnpcntop  15540  dvcj  15574  dvmptfsum  15590  dveflem  15591  ply1termlem  15607  plyaddlem1  15612  plymullem1  15613  plycolemc  15623  plycjlemc  15625  plyrecj  15628  dvply1  15630  reeff1olem  15636  eflt  15640  sin0pilem1  15646  ptolemy  15689  coseq0q4123  15699  coseq0negpitopi  15701  cos02pilt1  15716  cos11  15718  ioocosf1o  15719  rpcxpmul2  15778  cxplt  15781  cxple  15782  cxplt3  15785  apcxp2  15804  rprelogbmul  15820  rprelogbdiv  15822  pellexlem3  15847  dvdsppwf1o  15857  perfect  15869  lgsval  15877  lgsfcl2  15879  lgscllem  15880  lgsval2lem  15883  lgsdir2lem4  15904  lgsdir2lem5  15905  lgsdir2  15906  lgsne0  15911  gausslemma2dlem1a  15931  gausslemma2dlem1f1o  15933  2sqlem6  15993  2sqlem10  15998  umgrnloopv  16109  umgrvad2edg  16206  usgr1eop  16240  wlkvtxiedg  16340  wlkvtxiedgg  16341  upgredginwlk  16351  upgriswlkdc  16355  clwwlkccatlem  16395  eupth2lem3lem4fi  16468  pw1ndom3  16764  pw1map  16769  pwle2  16772  pwf1oexmid  16773  subctctexmid  16774  pw1nct  16777  peano4nninf  16784  nninfalllem1  16786  nninfall  16787  nninfsellemeq  16792  nninfsellemqall  16793  nnnninfex  16800  nninfnfiinf  16801  sbthom  16806  refeq  16808  isomninnlem  16814  trilpolemeq1  16824  trilpolemlt1  16825  trirec0  16828  apdiff  16832  iswomninnlem  16834  ismkvnnlem  16837  redcwlpolemeq1  16839  trimul0or  16845  ltlenmkv  16856  gfsumz  16869  gfsumcl  16870