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  3602  ifnefals  3648  intab  3955  exmid01  4286  exmidundif  4294  exmidundifim  4295  frirrg  4445  reg2exmidlema  4630  imadiflem  5406  fvco4  5714  fvmptt  5734  fcoconst  5814  funopsn  5825  f1imass  5910  fcof1  5919  fliftfun  5932  riotass2  5995  ovmpodxf  6142  dftpos4  6424  tfrlem1  6469  tfrlem3ag  6470  tfrlemibacc  6487  tfrlemibfn  6489  tfrlemi1  6493  tfrlemi14d  6494  tfr1onlem3ag  6498  tfr1onlembacc  6503  tfr1onlembfn  6505  tfr1onlemaccex  6509  tfrcllembacc  6516  tfrcllembfn  6518  tfrcllemaccex  6522  frecabcl  6560  nntr2  6666  dcdifsnid  6667  nnm00  6693  ecopovsymg  6798  ecopoverg  6800  th3qlem1  6801  mapss  6855  f1imaen2g  6962  pw2f1odclem  7015  xpen  7026  xpmapenlem  7030  phpm  7047  fidifsnen  7052  dif1enen  7062  fiunsnnn  7063  fin0  7067  fin0or  7068  findcard2d  7073  findcard2sd  7074  diffifi  7076  isinfinf  7079  tridc  7082  fimax2gtrilemstep  7083  fimax2gtri  7084  en2eqpr  7092  onunsnss  7102  unsnfidcex  7105  unsnfidcel  7106  undifdcss  7108  unfiin  7111  fisseneq  7119  ssfirab  7121  f1finf1o  7137  fidcenumlemrks  7143  fidcenumlemrk  7144  fidcenumlemr  7145  fidcenum  7146  suplub2ti  7191  supisolem  7198  ordiso2  7225  djudom  7283  omp1eomlem  7284  difinfsnlem  7289  difinfinf  7291  ctm  7299  ctssdclemn0  7300  enumct  7305  nnnninfeq  7318  nnnninfeq2  7319  nninfisol  7323  enomnilem  7328  finomni  7330  exmidomni  7332  fodju0  7337  ismkvnex  7345  enmkvlem  7351  enwomnilem  7359  pr2cv1  7391  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  exmidaclem  7413  exmidontriimlem1  7426  exmidontriimlem2  7427  exmidontriimlem3  7428  exmidontriimlem4  7429  exmidontriim  7430  netap  7463  exmidapne  7469  dfplpq2  7564  dfmpq2  7565  mulpipqqs  7583  nqpi  7588  distrnqg  7597  prarloclemarch  7628  enq0tr  7644  nqnq0pi  7648  nq0nn  7652  nnnq0lem1  7656  prarloclemup  7705  prarloclem3  7707  prarloclemcalc  7712  genplt2i  7720  addnqprllem  7737  addnqprulem  7738  appdivnq  7773  distrlem1prl  7792  distrlem1pru  7793  ltaddpr  7807  ltexprlemlol  7812  ltexprlemupu  7814  ltexprlemdisj  7816  addcanprleml  7824  ltaprlem  7828  addextpr  7831  recexprlemopu  7837  recexprlemdisj  7840  recexprlem1ssl  7843  aptiprleml  7849  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemopu  7858  cauappcvgprlemdisj  7861  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemopu  7881  caucvgprlemladdfu  7887  caucvgprprlemml  7904  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemopu  7909  caucvgprprlemexbt  7916  suplocexprlemru  7929  suplocexprlemloc  7931  suplocexprlemub  7933  suplocexprlemlub  7934  prsrlem1  7952  recexgt0sr  7983  mulgt0sr  7988  archsr  7992  caucvgsrlemcau  8003  caucvgsrlemoffcau  8008  caucvgsrlemoffres  8010  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  addcnsr  8044  mulcnsr  8045  mulcnsrec  8053  axmulcom  8081  nntopi  8104  axcaucvglemcau  8108  axcaucvglemres  8109  axpre-suploclemres  8111  axpre-suploc  8112  mpomulf  8159  axsuploc  8242  ltntri  8297  cnegexlem2  8345  cnegexlem3  8346  addsub4  8412  le2add  8614  lt2add  8615  lt2sub  8630  le2sub  8631  rereim  8756  apreim  8773  mulreim  8774  apcotr  8777  apadd1  8778  addext  8780  mulext1  8782  mulext  8784  apti  8792  aptap  8820  receuap  8839  rec11rap  8881  divdivdivap  8883  divadddivap  8897  divsubdivap  8898  rerecclap  8900  recgt0  9020  prodgt0gt0  9021  prodgt0  9022  prodge0  9024  lemulge11  9036  lt2mul2div  9049  ltrec  9053  lerec  9054  ltrec1  9058  lediv2a  9065  mulle0r  9114  sup3exmid  9127  zdiv  9558  eluzuzle  9754  supinfneg  9819  infsupneg  9820  infregelbex  9822  xrltso  10021  xnn0dcle  10027  xnn0letri  10028  npnflt  10040  nmnfgt  10043  z2ge  10051  xaddf  10069  xaddval  10070  xpncan  10096  xleadd1a  10098  xltadd1  10101  xaddge0  10103  xle2add  10104  xleaddadd  10112  ixxss1  10129  ixxss2  10130  elico2  10162  iccsupr  10191  fzass4  10287  fzrev  10309  fz0fzelfz0  10352  fzocatel  10434  elfzomelpfzo  10466  zsupcllemstep  10479  exbtwnzlemstep  10497  rebtwn2zlemstep  10502  qbtwnxr  10507  xqltnle  10517  apbtwnz  10524  btwnzge0  10550  modqid  10601  modqcyc  10611  modqcyc2  10612  modqaddabs  10614  modqaddmod  10615  mulqaddmodid  10616  modqmuladd  10618  modqltm1p1mod  10628  modqsubmod  10634  modqsubmodmod  10635  modaddmodlo  10640  modqmulmod  10641  modqmulmodr  10642  modqsubdir  10645  addmodlteq  10650  nninfinf  10695  iseqf1olemab  10754  iseqf1olemmo  10757  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  seqf1oglem1  10771  seqf1oglem2  10772  seqf1og  10773  exp3val  10793  expcl2lemap  10803  expap0  10821  expnegzap  10825  expmul  10836  leexp1a  10846  qsqeqor  10902  expnbnd  10915  nn0ltexp2  10961  nn0opth2  10976  facndiv  10991  faclbnd  10993  bcval5  11015  bcpasc  11018  hashennnuni  11031  hashunlem  11057  hashunsng  11061  hashprg  11062  fiprsshashgt1  11071  hashxp  11080  fimaxq  11081  zfz1isolemiso  11093  zfz1isolem1  11094  seq3coll  11096  iswrdiz  11110  wrdnval  11134  ccatlen  11162  ccatvalfn  11168  ccatsymb  11169  ccatalpha  11180  ccat2s1fstg  11215  swrdclg  11221  swrdsb0eq  11236  pfxwrdsymbg  11261  wrdind  11293  wrd2ind  11294  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12  11304  pfxccat3  11305  swrdccat  11306  shftlem  11367  shftfvalg  11369  shftfval  11372  2shfti  11382  caucvgrelemrec  11530  caucvgrelemcau  11531  caucvgre  11532  cvg1nlemcau  11535  cvg1nlemres  11536  resqrexlemcalc3  11567  resqrexlemcvg  11570  resqrexlemglsq  11573  resqrexlemga  11574  sqrtsq  11595  leabs  11625  absexpzap  11631  abslt  11639  absle  11640  abssubap0  11641  caubnd2  11668  icodiamlt  11731  maxleim  11756  maxabslemval  11759  maxleastlt  11766  rexico  11772  zmaxcl  11775  fimaxre2  11778  minmax  11781  xrmaxleim  11795  xrmaxiflemcl  11796  xrmaxifle  11797  xrmaxiflemlub  11799  xrmaxiflemval  11801  xrmaxleastlt  11807  xrmaxltsup  11809  xrmaxadd  11812  xrminmax  11816  xrbdtri  11827  climuni  11844  climshftlemg  11853  iserex  11890  climcau  11898  climrecvg1n  11899  climcvg1nlem  11900  sumeq2  11910  summodclem3  11931  zsumdc  11935  isumss  11942  fisumss  11943  sumsnf  11960  fsumconst  12005  modfsummod  12009  fsum00  12013  fsumabs  12016  fsumrelem  12022  fsumiun  12028  isumsplit  12042  divcnv  12048  geo2sum  12065  geoisumr  12069  cvgratz  12083  ntrivcvgap  12099  prodeq2  12108  prodmodclem2  12128  prodmodc  12129  zproddc  12130  fprodmul  12142  prodsnf  12143  fprodcl2lem  12156  fprodconst  12171  fprodap0  12172  fprodrec  12180  fprodap0f  12187  fprodle  12191  fprodmodd  12192  tanaddap  12290  zdvdsdc  12363  dvds2ln  12375  fsumdvds  12393  dvdsle  12395  dvdsext  12406  divalglemeunn  12472  divalglemex  12473  divalglemeuneg  12474  bitsfzo  12506  bitsmod  12507  bitsinv1lem  12512  bitsinv1  12513  dvdsbnd  12517  gcdsupex  12518  gcdsupcl  12519  dvdslegcd  12525  bezoutlemnewy  12557  bezoutlemstep  12558  bezoutlemmain  12559  bezoutlemzz  12563  bezoutlembz  12565  bezoutlembi  12566  bezoutlemle  12569  dfgcd3  12571  bezout  12572  dfgcd2  12575  dvdsmulgcd  12586  bezoutr  12593  uzwodc  12598  nninfctlemfo  12601  lcmval  12625  lcmcllem  12629  lcmneg  12636  ncoprmgcdne1b  12651  isprm2lem  12678  prmind2  12682  dvdsnprmd  12687  isprm5  12704  prmdvdsexp  12710  sqrt2irr  12724  oddpwdclemxy  12731  oddpwdclemdc  12735  nonsq  12769  pceu  12858  pcmul  12864  pc2dvds  12893  pcz  12895  pcprmpw2  12896  dvdsprmpweqle  12900  pcfac  12913  qexpz  12915  prmpwdvds  12918  1arith  12930  mul4sq  12957  4sqexercise2  12962  4sqlemsdc  12963  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemhom  13026  ennnfonelemfun  13028  ennnfonelemf1  13029  ennnfonelemim  13035  exmidunben  13037  ctiunctlemfo  13050  omiunct  13055  ssnnctlemct  13057  isstruct2r  13083  prdsval  13346  ismgm  13430  issgrp  13476  sgrppropd  13486  sgrpidmndm  13493  mndpropd  13513  issubmnd  13515  prdsidlem  13520  resmhm2b  13562  gsumwmhm  13571  isgrpinv  13627  grplmulf1o  13647  dfgrp3mlem  13671  grplactcnv  13675  pwssub  13686  mhmid  13692  mhmmnd  13693  ghmgrp  13695  mulgval  13699  mulgfng  13701  mulgnnp1  13707  mulgnn0dir  13729  mulgneg2  13733  mhmmulg  13740  grpissubg  13771  isnsg  13779  isnsg3  13784  nmzsubg  13787  ghmmhmb  13831  ghmpreima  13843  ghmnsgpreima  13846  ghmf1  13850  ghmf1o  13852  conjghm  13853  conjnmz  13856  conjnmzb  13857  ghmcmn  13904  gsumfzconst  13918  issrg  13968  srglmhm  13996  srgrmhm  13997  isring  14003  ringadd2  14030  ringlghm  14064  ringrghm  14065  oppr1g  14085  dvdsrvald  14097  dvdsrd  14098  dvdsrex  14102  dvdsrmul1  14106  unitgrp  14120  rhmopp  14180  subrgintm  14247  subrgpropd  14257  isdomn  14273  lmodprop2d  14352  lssvacl  14369  lssvsubcl  14370  lssvscl  14379  lsslss  14385  lss1d  14387  lsspropdg  14435  expghmap  14611  mulgghm2  14612  znunit  14663  znrrg  14664  mplvalcoe  14694  mplsubgfilemcl  14703  mplsubgfileminv  14704  mplsubgfi  14705  opnssneib  14870  restbasg  14882  restopn2  14897  iscnp4  14932  cnss2  14941  cnconst2  14947  cnptopresti  14952  cnptoprest2  14954  neitx  14982  uptx  14988  txrest  14990  txdis1cn  14992  xmetres2  15093  xblss2ps  15118  blhalf  15122  blssps  15141  blss  15142  blssexps  15143  blssex  15144  blin2  15146  metequiv2  15210  bdmetval  15214  metcnp3  15225  metcnp  15226  metcn  15228  metcnpi  15229  metcnpi2  15230  txmetcnp  15232  txmetcn  15233  qtopbas  15236  tgqioo  15269  mpomulcn  15280  fsumcncntop  15281  elcncf2  15288  mulcncflem  15321  mulcncf  15322  suplociccreex  15338  limcdifap  15376  cnplimcim  15381  cnplimccntop  15384  limccnpcntop  15389  dvcj  15423  dvmptfsum  15439  dveflem  15440  ply1termlem  15456  plyaddlem1  15461  plymullem1  15462  plycolemc  15472  plycjlemc  15474  plyrecj  15477  dvply1  15479  reeff1olem  15485  eflt  15489  sin0pilem1  15495  ptolemy  15538  coseq0q4123  15548  coseq0negpitopi  15550  cos02pilt1  15565  cos11  15567  ioocosf1o  15568  rpcxpmul2  15627  cxplt  15630  cxple  15631  cxplt3  15634  apcxp2  15653  rprelogbmul  15669  rprelogbdiv  15671  dvdsppwf1o  15703  perfect  15715  lgsval  15723  lgsfcl2  15725  lgscllem  15726  lgsval2lem  15729  lgsdir2lem4  15750  lgsdir2lem5  15751  lgsdir2  15752  lgsne0  15757  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  2sqlem6  15839  2sqlem10  15844  umgrnloopv  15955  umgrvad2edg  16050  usgr1eop  16084  wlkvtxiedg  16142  wlkvtxiedgg  16143  upgredginwlk  16153  upgriswlkdc  16157  clwwlkccatlem  16195  pw1ndom3  16525  2omap  16530  pw1map  16532  pwle2  16535  pwf1oexmid  16536  subctctexmid  16537  pw1nct  16540  peano4nninf  16544  nninfalllem1  16546  nninfall  16547  nninfsellemeq  16552  nninfsellemqall  16553  nnnninfex  16560  nninfnfiinf  16561  sbthom  16566  refeq  16568  isomninnlem  16570  trilpolemeq1  16580  trilpolemlt1  16581  trirec0  16584  apdiff  16588  iswomninnlem  16589  ismkvnnlem  16592  redcwlpolemeq1  16594  ltlenmkv  16610