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  1087  simp2lr  1091  simp3lr  1095  bilukdc  1440  dcun  3604  ifnefals  3650  intab  3957  exmid01  4288  exmidundif  4296  exmidundifim  4297  frirrg  4447  reg2exmidlema  4632  imadiflem  5409  fvco4  5718  fvmptt  5738  fcoconst  5818  funopsn  5830  f1imass  5915  fcof1  5924  fliftfun  5937  riotass2  6000  ovmpodxf  6147  dftpos4  6429  tfrlem1  6474  tfrlem3ag  6475  tfrlemibacc  6492  tfrlemibfn  6494  tfrlemi1  6498  tfrlemi14d  6499  tfr1onlem3ag  6503  tfr1onlembacc  6508  tfr1onlembfn  6510  tfr1onlemaccex  6514  tfrcllembacc  6521  tfrcllembfn  6523  tfrcllemaccex  6527  frecabcl  6565  nntr2  6671  dcdifsnid  6672  nnm00  6698  ecopovsymg  6803  ecopoverg  6805  th3qlem1  6806  mapss  6860  f1imaen2g  6967  pw2f1odclem  7020  xpen  7031  xpmapenlem  7035  phpm  7052  fidifsnen  7057  dif1enen  7069  fiunsnnn  7070  fin0  7074  fin0or  7075  findcard2d  7080  findcard2sd  7081  diffifi  7083  isinfinf  7086  tridc  7089  fimax2gtrilemstep  7090  fimax2gtri  7091  en2eqpr  7099  onunsnss  7109  unsnfidcex  7112  unsnfidcel  7113  undifdcss  7115  unfiin  7118  fisseneq  7127  ssfirab  7129  f1finf1o  7146  fidcenumlemrks  7152  fidcenumlemrk  7153  fidcenumlemr  7154  fidcenum  7155  suplub2ti  7200  supisolem  7207  ordiso2  7234  djudom  7292  omp1eomlem  7293  difinfsnlem  7298  difinfinf  7300  ctm  7308  ctssdclemn0  7309  enumct  7314  nnnninfeq  7327  nnnninfeq2  7328  nninfisol  7332  enomnilem  7337  finomni  7339  exmidomni  7341  fodju0  7346  ismkvnex  7354  enmkvlem  7360  enwomnilem  7368  pr2cv1  7400  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  exmidontriimlem1  7436  exmidontriimlem2  7437  exmidontriimlem3  7438  exmidontriimlem4  7439  exmidontriim  7440  netap  7473  exmidapne  7479  dfplpq2  7574  dfmpq2  7575  mulpipqqs  7593  nqpi  7598  distrnqg  7607  prarloclemarch  7638  enq0tr  7654  nqnq0pi  7658  nq0nn  7662  nnnq0lem1  7666  prarloclemup  7715  prarloclem3  7717  prarloclemcalc  7722  genplt2i  7730  addnqprllem  7747  addnqprulem  7748  appdivnq  7783  distrlem1prl  7802  distrlem1pru  7803  ltaddpr  7817  ltexprlemlol  7822  ltexprlemupu  7824  ltexprlemdisj  7826  addcanprleml  7834  ltaprlem  7838  addextpr  7841  recexprlemopu  7847  recexprlemdisj  7850  recexprlem1ssl  7853  aptiprleml  7859  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemdisj  7871  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemladdfu  7897  caucvgprprlemml  7914  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemexbt  7926  suplocexprlemru  7939  suplocexprlemloc  7941  suplocexprlemub  7943  suplocexprlemlub  7944  prsrlem1  7962  recexgt0sr  7993  mulgt0sr  7998  archsr  8002  caucvgsrlemcau  8013  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  addcnsr  8054  mulcnsr  8055  mulcnsrec  8063  axmulcom  8091  nntopi  8114  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  mpomulf  8169  axsuploc  8252  ltntri  8307  cnegexlem2  8355  cnegexlem3  8356  addsub4  8422  le2add  8624  lt2add  8625  lt2sub  8640  le2sub  8641  rereim  8766  apreim  8783  mulreim  8784  apcotr  8787  apadd1  8788  addext  8790  mulext1  8792  mulext  8794  apti  8802  aptap  8830  receuap  8849  rec11rap  8891  divdivdivap  8893  divadddivap  8907  divsubdivap  8908  rerecclap  8910  recgt0  9030  prodgt0gt0  9031  prodgt0  9032  prodge0  9034  lemulge11  9046  lt2mul2div  9059  ltrec  9063  lerec  9064  ltrec1  9068  lediv2a  9075  mulle0r  9124  sup3exmid  9137  zdiv  9568  eluzuzle  9764  supinfneg  9829  infsupneg  9830  infregelbex  9832  xrltso  10031  xnn0dcle  10037  xnn0letri  10038  npnflt  10050  nmnfgt  10053  z2ge  10061  xaddf  10079  xaddval  10080  xpncan  10106  xleadd1a  10108  xltadd1  10111  xaddge0  10113  xle2add  10114  xleaddadd  10122  ixxss1  10139  ixxss2  10140  elico2  10172  iccsupr  10201  fzass4  10297  fzrev  10319  fz0fzelfz0  10362  fzocatel  10445  elfzomelpfzo  10477  zsupcllemstep  10490  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  qbtwnxr  10518  xqltnle  10528  apbtwnz  10535  btwnzge0  10561  modqid  10612  modqcyc  10622  modqcyc2  10623  modqaddabs  10625  modqaddmod  10626  mulqaddmodid  10627  modqmuladd  10629  modqltm1p1mod  10639  modqsubmod  10645  modqsubmodmod  10646  modaddmodlo  10651  modqmulmod  10652  modqmulmodr  10653  modqsubdir  10656  addmodlteq  10661  nninfinf  10706  iseqf1olemab  10765  iseqf1olemmo  10768  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  seqf1oglem1  10782  seqf1oglem2  10783  seqf1og  10784  exp3val  10804  expcl2lemap  10814  expap0  10832  expnegzap  10836  expmul  10847  leexp1a  10857  qsqeqor  10913  expnbnd  10926  nn0ltexp2  10972  nn0opth2  10987  facndiv  11002  faclbnd  11004  bcval5  11026  bcpasc  11029  hashennnuni  11042  hashunlem  11068  hashunsng  11072  hashprg  11073  fiprsshashgt1  11082  hashxp  11091  fimaxq  11092  zfz1isolemiso  11104  zfz1isolem1  11105  seq3coll  11107  iswrdiz  11124  wrdnval  11148  ccatlen  11176  ccatvalfn  11182  ccatsymb  11183  ccatalpha  11194  ccat2s1fstg  11229  swrdclg  11235  swrdsb0eq  11250  pfxwrdsymbg  11275  wrdind  11307  wrd2ind  11308  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12  11318  pfxccat3  11319  swrdccat  11320  shftlem  11381  shftfvalg  11383  shftfval  11386  2shfti  11396  caucvgrelemrec  11544  caucvgrelemcau  11545  caucvgre  11546  cvg1nlemcau  11549  cvg1nlemres  11550  resqrexlemcalc3  11581  resqrexlemcvg  11584  resqrexlemglsq  11587  resqrexlemga  11588  sqrtsq  11609  leabs  11639  absexpzap  11645  abslt  11653  absle  11654  abssubap0  11655  caubnd2  11682  icodiamlt  11745  maxleim  11770  maxabslemval  11773  maxleastlt  11780  rexico  11786  zmaxcl  11789  fimaxre2  11792  minmax  11795  xrmaxleim  11809  xrmaxiflemcl  11810  xrmaxifle  11811  xrmaxiflemlub  11813  xrmaxiflemval  11815  xrmaxleastlt  11821  xrmaxltsup  11823  xrmaxadd  11826  xrminmax  11830  xrbdtri  11841  climuni  11858  climshftlemg  11867  iserex  11904  climcau  11912  climrecvg1n  11913  climcvg1nlem  11914  sumeq2  11924  summodclem3  11946  zsumdc  11950  isumss  11957  fisumss  11958  sumsnf  11975  fsumconst  12020  modfsummod  12024  fsum00  12028  fsumabs  12031  fsumrelem  12037  fsumiun  12043  isumsplit  12057  divcnv  12063  geo2sum  12080  geoisumr  12084  cvgratz  12098  ntrivcvgap  12114  prodeq2  12123  prodmodclem2  12143  prodmodc  12144  zproddc  12145  fprodmul  12157  prodsnf  12158  fprodcl2lem  12171  fprodconst  12186  fprodap0  12187  fprodrec  12195  fprodap0f  12202  fprodle  12206  fprodmodd  12207  tanaddap  12305  zdvdsdc  12378  dvds2ln  12390  fsumdvds  12408  dvdsle  12410  dvdsext  12421  divalglemeunn  12487  divalglemex  12488  divalglemeuneg  12489  bitsfzo  12521  bitsmod  12522  bitsinv1lem  12527  bitsinv1  12528  dvdsbnd  12532  gcdsupex  12533  gcdsupcl  12534  dvdslegcd  12540  bezoutlemnewy  12572  bezoutlemstep  12573  bezoutlemmain  12574  bezoutlemzz  12578  bezoutlembz  12580  bezoutlembi  12581  bezoutlemle  12584  dfgcd3  12586  bezout  12587  dfgcd2  12590  dvdsmulgcd  12601  bezoutr  12608  uzwodc  12613  nninfctlemfo  12616  lcmval  12640  lcmcllem  12644  lcmneg  12651  ncoprmgcdne1b  12666  isprm2lem  12693  prmind2  12697  dvdsnprmd  12702  isprm5  12719  prmdvdsexp  12725  sqrt2irr  12739  oddpwdclemxy  12746  oddpwdclemdc  12750  nonsq  12784  pceu  12873  pcmul  12879  pc2dvds  12908  pcz  12910  pcprmpw2  12911  dvdsprmpweqle  12915  pcfac  12928  qexpz  12930  prmpwdvds  12933  1arith  12945  mul4sq  12972  4sqexercise2  12977  4sqlemsdc  12978  ennnfonelemkh  13038  ennnfonelemhf1o  13039  ennnfonelemhom  13041  ennnfonelemfun  13043  ennnfonelemf1  13044  ennnfonelemim  13050  exmidunben  13052  ctiunctlemfo  13065  omiunct  13070  ssnnctlemct  13072  isstruct2r  13098  prdsval  13361  ismgm  13445  issgrp  13491  sgrppropd  13501  sgrpidmndm  13508  mndpropd  13528  issubmnd  13530  prdsidlem  13535  resmhm2b  13577  gsumwmhm  13586  isgrpinv  13642  grplmulf1o  13662  dfgrp3mlem  13686  grplactcnv  13690  pwssub  13701  mhmid  13707  mhmmnd  13708  ghmgrp  13710  mulgval  13714  mulgfng  13716  mulgnnp1  13722  mulgnn0dir  13744  mulgneg2  13748  mhmmulg  13755  grpissubg  13786  isnsg  13794  isnsg3  13799  nmzsubg  13802  ghmmhmb  13846  ghmpreima  13858  ghmnsgpreima  13861  ghmf1  13865  ghmf1o  13867  conjghm  13868  conjnmz  13871  conjnmzb  13872  ghmcmn  13919  gsumfzconst  13933  issrg  13984  srglmhm  14012  srgrmhm  14013  isring  14019  ringadd2  14046  ringlghm  14080  ringrghm  14081  oppr1g  14101  dvdsrvald  14113  dvdsrd  14114  dvdsrex  14118  dvdsrmul1  14122  unitgrp  14136  rhmopp  14196  subrgintm  14263  subrgpropd  14273  isdomn  14289  lmodprop2d  14368  lssvacl  14385  lssvsubcl  14386  lssvscl  14395  lsslss  14401  lss1d  14403  lsspropdg  14451  expghmap  14627  mulgghm2  14628  znunit  14679  znrrg  14680  mplvalcoe  14710  mplsubgfilemcl  14719  mplsubgfileminv  14720  mplsubgfi  14721  opnssneib  14886  restbasg  14898  restopn2  14913  iscnp4  14948  cnss2  14957  cnconst2  14963  cnptopresti  14968  cnptoprest2  14970  neitx  14998  uptx  15004  txrest  15006  txdis1cn  15008  xmetres2  15109  xblss2ps  15134  blhalf  15138  blssps  15157  blss  15158  blssexps  15159  blssex  15160  blin2  15162  metequiv2  15226  bdmetval  15230  metcnp3  15241  metcnp  15242  metcn  15244  metcnpi  15245  metcnpi2  15246  txmetcnp  15248  txmetcn  15249  qtopbas  15252  tgqioo  15285  mpomulcn  15296  fsumcncntop  15297  elcncf2  15304  mulcncflem  15337  mulcncf  15338  suplociccreex  15354  limcdifap  15392  cnplimcim  15397  cnplimccntop  15400  limccnpcntop  15405  dvcj  15439  dvmptfsum  15455  dveflem  15456  ply1termlem  15472  plyaddlem1  15477  plymullem1  15478  plycolemc  15488  plycjlemc  15490  plyrecj  15493  dvply1  15495  reeff1olem  15501  eflt  15505  sin0pilem1  15511  ptolemy  15554  coseq0q4123  15564  coseq0negpitopi  15566  cos02pilt1  15581  cos11  15583  ioocosf1o  15584  rpcxpmul2  15643  cxplt  15646  cxple  15647  cxplt3  15650  apcxp2  15669  rprelogbmul  15685  rprelogbdiv  15687  dvdsppwf1o  15719  perfect  15731  lgsval  15739  lgsfcl2  15741  lgscllem  15742  lgsval2lem  15745  lgsdir2lem4  15766  lgsdir2lem5  15767  lgsdir2  15768  lgsne0  15773  gausslemma2dlem1a  15793  gausslemma2dlem1f1o  15795  2sqlem6  15855  2sqlem10  15860  umgrnloopv  15971  umgrvad2edg  16068  usgr1eop  16102  wlkvtxiedg  16202  wlkvtxiedgg  16203  upgredginwlk  16213  upgriswlkdc  16217  clwwlkccatlem  16257  eupth2lem3lem4fi  16330  pw1ndom3  16615  2omap  16620  pw1map  16622  pwle2  16625  pwf1oexmid  16626  subctctexmid  16627  pw1nct  16630  peano4nninf  16634  nninfalllem1  16636  nninfall  16637  nninfsellemeq  16642  nninfsellemqall  16643  nnnninfex  16650  nninfnfiinf  16651  sbthom  16656  refeq  16658  isomninnlem  16660  trilpolemeq1  16670  trilpolemlt1  16671  trirec0  16674  apdiff  16678  iswomninnlem  16680  ismkvnnlem  16683  redcwlpolemeq1  16685  ltlenmkv  16701  gfsumcl  16714