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  3951  exmid01  4281  exmidundif  4289  exmidundifim  4290  frirrg  4440  reg2exmidlema  4625  imadiflem  5399  fvco4  5705  fvmptt  5725  fcoconst  5805  funopsn  5816  f1imass  5897  fcof1  5906  fliftfun  5919  riotass2  5982  ovmpodxf  6129  dftpos4  6407  tfrlem1  6452  tfrlem3ag  6453  tfrlemibacc  6470  tfrlemibfn  6472  tfrlemi1  6476  tfrlemi14d  6477  tfr1onlem3ag  6481  tfr1onlembacc  6486  tfr1onlembfn  6488  tfr1onlemaccex  6492  tfrcllembacc  6499  tfrcllembfn  6501  tfrcllemaccex  6505  frecabcl  6543  nntr2  6647  dcdifsnid  6648  nnm00  6674  ecopovsymg  6779  ecopoverg  6781  th3qlem1  6782  mapss  6836  f1imaen2g  6943  pw2f1odclem  6991  xpen  7002  xpmapenlem  7006  phpm  7023  fidifsnen  7028  dif1enen  7038  fiunsnnn  7039  fin0  7043  fin0or  7044  findcard2d  7049  findcard2sd  7050  diffifi  7052  isinfinf  7055  tridc  7057  fimax2gtrilemstep  7058  fimax2gtri  7059  en2eqpr  7065  onunsnss  7075  unsnfidcex  7078  unsnfidcel  7079  undifdcss  7081  unfiin  7084  fisseneq  7092  ssfirab  7094  f1finf1o  7110  fidcenumlemrks  7116  fidcenumlemrk  7117  fidcenumlemr  7118  fidcenum  7119  suplub2ti  7164  supisolem  7171  ordiso2  7198  djudom  7256  omp1eomlem  7257  difinfsnlem  7262  difinfinf  7264  ctm  7272  ctssdclemn0  7273  enumct  7278  nnnninfeq  7291  nnnninfeq2  7292  nninfisol  7296  enomnilem  7301  finomni  7303  exmidomni  7305  fodju0  7310  ismkvnex  7318  enmkvlem  7324  enwomnilem  7332  pr2cv1  7364  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  exmidaclem  7386  exmidontriimlem1  7399  exmidontriimlem2  7400  exmidontriimlem3  7401  exmidontriimlem4  7402  exmidontriim  7403  netap  7436  exmidapne  7442  dfplpq2  7537  dfmpq2  7538  mulpipqqs  7556  nqpi  7561  distrnqg  7570  prarloclemarch  7601  enq0tr  7617  nqnq0pi  7621  nq0nn  7625  nnnq0lem1  7629  prarloclemup  7678  prarloclem3  7680  prarloclemcalc  7685  genplt2i  7693  addnqprllem  7710  addnqprulem  7711  appdivnq  7746  distrlem1prl  7765  distrlem1pru  7766  ltaddpr  7780  ltexprlemlol  7785  ltexprlemupu  7787  ltexprlemdisj  7789  addcanprleml  7797  ltaprlem  7801  addextpr  7804  recexprlemopu  7810  recexprlemdisj  7813  recexprlem1ssl  7816  aptiprleml  7822  cauappcvgprlemm  7828  cauappcvgprlemopl  7829  cauappcvgprlemlol  7830  cauappcvgprlemopu  7831  cauappcvgprlemdisj  7834  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  caucvgprlemm  7851  caucvgprlemopl  7852  caucvgprlemlol  7853  caucvgprlemopu  7854  caucvgprlemladdfu  7860  caucvgprprlemml  7877  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemopu  7882  caucvgprprlemexbt  7889  suplocexprlemru  7902  suplocexprlemloc  7904  suplocexprlemub  7906  suplocexprlemlub  7907  prsrlem1  7925  recexgt0sr  7956  mulgt0sr  7961  archsr  7965  caucvgsrlemcau  7976  caucvgsrlemoffcau  7981  caucvgsrlemoffres  7983  suplocsrlemb  7989  suplocsrlempr  7990  suplocsrlem  7991  addcnsr  8017  mulcnsr  8018  mulcnsrec  8026  axmulcom  8054  nntopi  8077  axcaucvglemcau  8081  axcaucvglemres  8082  axpre-suploclemres  8084  axpre-suploc  8085  mpomulf  8132  axsuploc  8215  ltntri  8270  cnegexlem2  8318  cnegexlem3  8319  addsub4  8385  le2add  8587  lt2add  8588  lt2sub  8603  le2sub  8604  rereim  8729  apreim  8746  mulreim  8747  apcotr  8750  apadd1  8751  addext  8753  mulext1  8755  mulext  8757  apti  8765  aptap  8793  receuap  8812  rec11rap  8854  divdivdivap  8856  divadddivap  8870  divsubdivap  8871  rerecclap  8873  recgt0  8993  prodgt0gt0  8994  prodgt0  8995  prodge0  8997  lemulge11  9009  lt2mul2div  9022  ltrec  9026  lerec  9027  ltrec1  9031  lediv2a  9038  mulle0r  9087  sup3exmid  9100  zdiv  9531  eluzuzle  9726  supinfneg  9786  infsupneg  9787  infregelbex  9789  xrltso  9988  xnn0dcle  9994  xnn0letri  9995  npnflt  10007  nmnfgt  10010  z2ge  10018  xaddf  10036  xaddval  10037  xpncan  10063  xleadd1a  10065  xltadd1  10068  xaddge0  10070  xle2add  10071  xleaddadd  10079  ixxss1  10096  ixxss2  10097  elico2  10129  iccsupr  10158  fzass4  10254  fzrev  10276  fz0fzelfz0  10319  fzocatel  10400  elfzomelpfzo  10432  zsupcllemstep  10444  exbtwnzlemstep  10462  rebtwn2zlemstep  10467  qbtwnxr  10472  xqltnle  10482  apbtwnz  10489  btwnzge0  10515  modqid  10566  modqcyc  10576  modqcyc2  10577  modqaddabs  10579  modqaddmod  10580  mulqaddmodid  10581  modqmuladd  10583  modqltm1p1mod  10593  modqsubmod  10599  modqsubmodmod  10600  modaddmodlo  10605  modqmulmod  10606  modqmulmodr  10607  modqsubdir  10610  addmodlteq  10615  nninfinf  10660  iseqf1olemab  10719  iseqf1olemmo  10722  iseqf1olemjpcl  10725  iseqf1olemqpcl  10726  seqf1oglem1  10736  seqf1oglem2  10737  seqf1og  10738  exp3val  10758  expcl2lemap  10768  expap0  10786  expnegzap  10790  expmul  10801  leexp1a  10811  qsqeqor  10867  expnbnd  10880  nn0ltexp2  10926  nn0opth2  10941  facndiv  10956  faclbnd  10958  bcval5  10980  bcpasc  10983  hashennnuni  10996  hashunlem  11021  hashunsng  11024  hashprg  11025  fiprsshashgt1  11034  hashxp  11043  fimaxq  11044  zfz1isolemiso  11056  zfz1isolem1  11057  seq3coll  11059  iswrdiz  11073  wrdnval  11097  ccatlen  11125  ccatvalfn  11131  ccatsymb  11132  swrdclg  11177  swrdsb0eq  11192  pfxwrdsymbg  11217  wrdind  11249  wrd2ind  11250  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatin12  11260  pfxccat3  11261  swrdccat  11262  shftlem  11322  shftfvalg  11324  shftfval  11327  2shfti  11337  caucvgrelemrec  11485  caucvgrelemcau  11486  caucvgre  11487  cvg1nlemcau  11490  cvg1nlemres  11491  resqrexlemcalc3  11522  resqrexlemcvg  11525  resqrexlemglsq  11528  resqrexlemga  11529  sqrtsq  11550  leabs  11580  absexpzap  11586  abslt  11594  absle  11595  abssubap0  11596  caubnd2  11623  icodiamlt  11686  maxleim  11711  maxabslemval  11714  maxleastlt  11721  rexico  11727  zmaxcl  11730  fimaxre2  11733  minmax  11736  xrmaxleim  11750  xrmaxiflemcl  11751  xrmaxifle  11752  xrmaxiflemlub  11754  xrmaxiflemval  11756  xrmaxleastlt  11762  xrmaxltsup  11764  xrmaxadd  11767  xrminmax  11771  xrbdtri  11782  climuni  11799  climshftlemg  11808  iserex  11845  climcau  11853  climrecvg1n  11854  climcvg1nlem  11855  sumeq2  11865  summodclem3  11886  zsumdc  11890  isumss  11897  fisumss  11898  sumsnf  11915  fsumconst  11960  modfsummod  11964  fsum00  11968  fsumabs  11971  fsumrelem  11977  fsumiun  11983  isumsplit  11997  divcnv  12003  geo2sum  12020  geoisumr  12024  cvgratz  12038  ntrivcvgap  12054  prodeq2  12063  prodmodclem2  12083  prodmodc  12084  zproddc  12085  fprodmul  12097  prodsnf  12098  fprodcl2lem  12111  fprodconst  12126  fprodap0  12127  fprodrec  12135  fprodap0f  12142  fprodle  12146  fprodmodd  12147  tanaddap  12245  zdvdsdc  12318  dvds2ln  12330  fsumdvds  12348  dvdsle  12350  dvdsext  12361  divalglemeunn  12427  divalglemex  12428  divalglemeuneg  12429  bitsfzo  12461  bitsmod  12462  bitsinv1lem  12467  bitsinv1  12468  dvdsbnd  12472  gcdsupex  12473  gcdsupcl  12474  dvdslegcd  12480  bezoutlemnewy  12512  bezoutlemstep  12513  bezoutlemmain  12514  bezoutlemzz  12518  bezoutlembz  12520  bezoutlembi  12521  bezoutlemle  12524  dfgcd3  12526  bezout  12527  dfgcd2  12530  dvdsmulgcd  12541  bezoutr  12548  uzwodc  12553  nninfctlemfo  12556  lcmval  12580  lcmcllem  12584  lcmneg  12591  ncoprmgcdne1b  12606  isprm2lem  12633  prmind2  12637  dvdsnprmd  12642  isprm5  12659  prmdvdsexp  12665  sqrt2irr  12679  oddpwdclemxy  12686  oddpwdclemdc  12690  nonsq  12724  pceu  12813  pcmul  12819  pc2dvds  12848  pcz  12850  pcprmpw2  12851  dvdsprmpweqle  12855  pcfac  12868  qexpz  12870  prmpwdvds  12873  1arith  12885  mul4sq  12912  4sqexercise2  12917  4sqlemsdc  12918  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemhom  12981  ennnfonelemfun  12983  ennnfonelemf1  12984  ennnfonelemim  12990  exmidunben  12992  ctiunctlemfo  13005  omiunct  13010  ssnnctlemct  13012  isstruct2r  13038  prdsval  13301  ismgm  13385  issgrp  13431  sgrppropd  13441  sgrpidmndm  13448  mndpropd  13468  issubmnd  13470  prdsidlem  13475  resmhm2b  13517  gsumwmhm  13526  isgrpinv  13582  grplmulf1o  13602  dfgrp3mlem  13626  grplactcnv  13630  pwssub  13641  mhmid  13647  mhmmnd  13648  ghmgrp  13650  mulgval  13654  mulgfng  13656  mulgnnp1  13662  mulgnn0dir  13684  mulgneg2  13688  mhmmulg  13695  grpissubg  13726  isnsg  13734  isnsg3  13739  nmzsubg  13742  ghmmhmb  13786  ghmpreima  13798  ghmnsgpreima  13801  ghmf1  13805  ghmf1o  13807  conjghm  13808  conjnmz  13811  conjnmzb  13812  ghmcmn  13859  gsumfzconst  13873  issrg  13923  srglmhm  13951  srgrmhm  13952  isring  13958  ringadd2  13985  ringlghm  14019  ringrghm  14020  oppr1g  14040  reldvdsrsrg  14050  dvdsrvald  14051  dvdsrd  14052  dvdsrex  14056  dvdsrmul1  14060  unitgrp  14074  rhmopp  14134  subrgintm  14201  subrgpropd  14211  isdomn  14227  lmodprop2d  14306  lssvacl  14323  lssvsubcl  14324  lssvscl  14333  lsslss  14339  lss1d  14341  lsspropdg  14389  expghmap  14565  mulgghm2  14566  znunit  14617  znrrg  14618  mplvalcoe  14648  mplsubgfilemcl  14657  mplsubgfileminv  14658  mplsubgfi  14659  opnssneib  14824  restbasg  14836  restopn2  14851  iscnp4  14886  cnss2  14895  cnconst2  14901  cnptopresti  14906  cnptoprest2  14908  neitx  14936  uptx  14942  txrest  14944  txdis1cn  14946  xmetres2  15047  xblss2ps  15072  blhalf  15076  blssps  15095  blss  15096  blssexps  15097  blssex  15098  blin2  15100  metequiv2  15164  bdmetval  15168  metcnp3  15179  metcnp  15180  metcn  15182  metcnpi  15183  metcnpi2  15184  txmetcnp  15186  txmetcn  15187  qtopbas  15190  tgqioo  15223  mpomulcn  15234  fsumcncntop  15235  elcncf2  15242  mulcncflem  15275  mulcncf  15276  suplociccreex  15292  limcdifap  15330  cnplimcim  15335  cnplimccntop  15338  limccnpcntop  15343  dvcj  15377  dvmptfsum  15393  dveflem  15394  ply1termlem  15410  plyaddlem1  15415  plymullem1  15416  plycolemc  15426  plycjlemc  15428  plyrecj  15431  dvply1  15433  reeff1olem  15439  eflt  15443  sin0pilem1  15449  ptolemy  15492  coseq0q4123  15502  coseq0negpitopi  15504  cos02pilt1  15519  cos11  15521  ioocosf1o  15522  rpcxpmul2  15581  cxplt  15584  cxple  15585  cxplt3  15588  apcxp2  15607  rprelogbmul  15623  rprelogbdiv  15625  dvdsppwf1o  15657  perfect  15669  lgsval  15677  lgsfcl2  15679  lgscllem  15680  lgsval2lem  15683  lgsdir2lem4  15704  lgsdir2lem5  15705  lgsdir2  15706  lgsne0  15711  gausslemma2dlem1a  15731  gausslemma2dlem1f1o  15733  2sqlem6  15793  2sqlem10  15798  umgrnloopv  15908  umgrvad2edg  16003  wlkvtxiedgg  16042  2omap  16318  pw1map  16320  pwle2  16323  pwf1oexmid  16324  subctctexmid  16325  pw1nct  16328  peano4nninf  16331  nninfalllem1  16333  nninfall  16334  nninfsellemeq  16339  nninfsellemqall  16340  nnnninfex  16347  nninfnfiinf  16348  sbthom  16353  refeq  16355  isomninnlem  16357  trilpolemeq1  16367  trilpolemlt1  16368  trirec0  16371  apdiff  16375  iswomninnlem  16376  ismkvnnlem  16379  redcwlpolemeq1  16381  ltlenmkv  16397