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  1061  simp2lr  1065  simp3lr  1069  bilukdc  1396  dcun  3534  intab  3874  exmid01  4199  exmidundif  4207  exmidundifim  4208  frirrg  4351  reg2exmidlema  4534  imadiflem  5296  fvco4  5589  fvmptt  5608  fcoconst  5688  f1imass  5775  fcof1  5784  fliftfun  5797  riotass2  5857  ovmpodxf  6000  dftpos4  6264  tfrlem1  6309  tfrlem3ag  6310  tfrlemibacc  6327  tfrlemibfn  6329  tfrlemi1  6333  tfrlemi14d  6334  tfr1onlem3ag  6338  tfr1onlembacc  6343  tfr1onlembfn  6345  tfr1onlemaccex  6349  tfrcllembacc  6356  tfrcllembfn  6358  tfrcllemaccex  6362  frecabcl  6400  nntr2  6504  dcdifsnid  6505  nnm00  6531  ecopovsymg  6634  ecopoverg  6636  th3qlem1  6637  mapss  6691  f1imaen2g  6793  xpen  6845  xpmapenlem  6849  phpm  6865  fidifsnen  6870  dif1enen  6880  fiunsnnn  6881  fin0  6885  fin0or  6886  findcard2d  6891  findcard2sd  6892  diffifi  6894  isinfinf  6897  tridc  6899  fimax2gtrilemstep  6900  fimax2gtri  6901  en2eqpr  6907  onunsnss  6916  unsnfidcex  6919  unsnfidcel  6920  undifdcss  6922  unfiin  6925  fisseneq  6931  ssfirab  6933  f1finf1o  6946  fidcenumlemrks  6952  fidcenumlemrk  6953  fidcenumlemr  6954  fidcenum  6955  suplub2ti  7000  supisolem  7007  ordiso2  7034  djudom  7092  omp1eomlem  7093  difinfsnlem  7098  difinfinf  7100  ctm  7108  ctssdclemn0  7109  enumct  7114  nnnninfeq  7126  nnnninfeq2  7127  nninfisol  7131  enomnilem  7136  finomni  7138  exmidomni  7140  fodju0  7145  ismkvnex  7153  enmkvlem  7159  enwomnilem  7167  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidaclem  7207  exmidontriimlem1  7220  exmidontriimlem2  7221  exmidontriimlem3  7222  exmidontriimlem4  7223  exmidontriim  7224  netap  7253  exmidapne  7259  dfplpq2  7353  dfmpq2  7354  mulpipqqs  7372  nqpi  7377  distrnqg  7386  prarloclemarch  7417  enq0tr  7433  nqnq0pi  7437  nq0nn  7441  nnnq0lem1  7445  prarloclemup  7494  prarloclem3  7496  prarloclemcalc  7501  genplt2i  7509  addnqprllem  7526  addnqprulem  7527  appdivnq  7562  distrlem1prl  7581  distrlem1pru  7582  ltaddpr  7596  ltexprlemlol  7601  ltexprlemupu  7603  ltexprlemdisj  7605  addcanprleml  7613  ltaprlem  7617  addextpr  7620  recexprlemopu  7626  recexprlemdisj  7629  recexprlem1ssl  7632  aptiprleml  7638  cauappcvgprlemm  7644  cauappcvgprlemopl  7645  cauappcvgprlemlol  7646  cauappcvgprlemopu  7647  cauappcvgprlemdisj  7650  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemlol  7669  caucvgprlemopu  7670  caucvgprlemladdfu  7676  caucvgprprlemml  7693  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemopu  7698  caucvgprprlemexbt  7705  suplocexprlemru  7718  suplocexprlemloc  7720  suplocexprlemub  7722  suplocexprlemlub  7723  prsrlem1  7741  recexgt0sr  7772  mulgt0sr  7777  archsr  7781  caucvgsrlemcau  7792  caucvgsrlemoffcau  7797  caucvgsrlemoffres  7799  suplocsrlemb  7805  suplocsrlempr  7806  suplocsrlem  7807  addcnsr  7833  mulcnsr  7834  mulcnsrec  7842  axmulcom  7870  nntopi  7893  axcaucvglemcau  7897  axcaucvglemres  7898  axpre-suploclemres  7900  axpre-suploc  7901  axsuploc  8030  ltntri  8085  cnegexlem2  8133  cnegexlem3  8134  addsub4  8200  le2add  8401  lt2add  8402  lt2sub  8417  le2sub  8418  rereim  8543  apreim  8560  mulreim  8561  apcotr  8564  apadd1  8565  addext  8567  mulext1  8569  mulext  8571  apti  8579  aptap  8607  receuap  8626  rec11rap  8668  divdivdivap  8670  divadddivap  8684  divsubdivap  8685  rerecclap  8687  recgt0  8807  prodgt0gt0  8808  prodgt0  8809  prodge0  8811  lemulge11  8823  lt2mul2div  8836  ltrec  8840  lerec  8841  ltrec1  8845  lediv2a  8852  mulle0r  8901  sup3exmid  8914  zdiv  9341  eluzuzle  9536  supinfneg  9595  infsupneg  9596  infregelbex  9598  xrltso  9796  xnn0dcle  9802  xnn0letri  9803  npnflt  9815  nmnfgt  9818  z2ge  9826  xaddf  9844  xaddval  9845  xpncan  9871  xleadd1a  9873  xltadd1  9876  xaddge0  9878  xle2add  9879  xleaddadd  9887  ixxss1  9904  ixxss2  9905  elico2  9937  iccsupr  9966  fzass4  10062  fzrev  10084  fz0fzelfz0  10127  fzocatel  10199  elfzomelpfzo  10231  exbtwnzlemstep  10248  rebtwn2zlemstep  10253  qbtwnxr  10258  apbtwnz  10274  btwnzge0  10300  modqid  10349  modqcyc  10359  modqcyc2  10360  modqaddabs  10362  modqaddmod  10363  mulqaddmodid  10364  modqmuladd  10366  modqltm1p1mod  10376  modqsubmod  10382  modqsubmodmod  10383  modaddmodlo  10388  modqmulmod  10389  modqmulmodr  10390  modqsubdir  10393  addmodlteq  10398  iseqf1olemab  10489  iseqf1olemmo  10492  iseqf1olemjpcl  10495  iseqf1olemqpcl  10496  exp3val  10522  expcl2lemap  10532  expap0  10550  expnegzap  10554  expmul  10565  leexp1a  10575  qsqeqor  10631  expnbnd  10644  nn0ltexp2  10689  nn0opth2  10704  facndiv  10719  faclbnd  10721  bcval5  10743  bcpasc  10746  hashennnuni  10759  hashunlem  10784  hashunsng  10787  hashprg  10788  fiprsshashgt1  10797  hashxp  10806  fimaxq  10807  zfz1isolemiso  10819  zfz1isolem1  10820  seq3coll  10822  shftlem  10825  shftfvalg  10827  shftfval  10830  2shfti  10840  caucvgrelemrec  10988  caucvgrelemcau  10989  caucvgre  10990  cvg1nlemcau  10993  cvg1nlemres  10994  resqrexlemcalc3  11025  resqrexlemcvg  11028  resqrexlemglsq  11031  resqrexlemga  11032  sqrtsq  11053  leabs  11083  absexpzap  11089  abslt  11097  absle  11098  abssubap0  11099  caubnd2  11126  icodiamlt  11189  maxleim  11214  maxabslemval  11217  maxleastlt  11224  rexico  11230  zmaxcl  11233  fimaxre2  11235  minmax  11238  xrmaxleim  11252  xrmaxiflemcl  11253  xrmaxifle  11254  xrmaxiflemlub  11256  xrmaxiflemval  11258  xrmaxleastlt  11264  xrmaxltsup  11266  xrmaxadd  11269  xrminmax  11273  xrbdtri  11284  climuni  11301  climshftlemg  11310  iserex  11347  climcau  11355  climrecvg1n  11356  climcvg1nlem  11357  sumeq2  11367  summodclem3  11388  zsumdc  11392  isumss  11399  fisumss  11400  sumsnf  11417  fsumconst  11462  modfsummod  11466  fsum00  11470  fsumabs  11473  fsumrelem  11479  fsumiun  11485  isumsplit  11499  divcnv  11505  geo2sum  11522  geoisumr  11526  cvgratz  11540  ntrivcvgap  11556  prodeq2  11565  prodmodclem2  11585  prodmodc  11586  zproddc  11587  fprodmul  11599  prodsnf  11600  fprodcl2lem  11613  fprodconst  11628  fprodap0  11629  fprodrec  11637  fprodap0f  11644  fprodle  11648  fprodmodd  11649  tanaddap  11747  zdvdsdc  11819  dvds2ln  11831  dvdsle  11850  dvdsext  11861  divalglemeunn  11926  divalglemex  11927  divalglemeuneg  11928  zsupcllemstep  11946  dvdsbnd  11957  gcdsupex  11958  gcdsupcl  11959  dvdslegcd  11965  bezoutlemnewy  11997  bezoutlemstep  11998  bezoutlemmain  11999  bezoutlemzz  12003  bezoutlembz  12005  bezoutlembi  12006  bezoutlemle  12009  dfgcd3  12011  bezout  12012  dfgcd2  12015  dvdsmulgcd  12026  bezoutr  12033  uzwodc  12038  lcmval  12063  lcmcllem  12067  lcmneg  12074  ncoprmgcdne1b  12089  isprm2lem  12116  prmind2  12120  dvdsnprmd  12125  isprm5  12142  prmdvdsexp  12148  sqrt2irr  12162  oddpwdclemxy  12169  oddpwdclemdc  12173  nonsq  12207  pceu  12295  pcmul  12301  pc2dvds  12329  pcz  12331  pcprmpw2  12332  dvdsprmpweqle  12336  pcfac  12348  qexpz  12350  prmpwdvds  12353  1arith  12365  mul4sq  12392  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemhom  12416  ennnfonelemfun  12418  ennnfonelemf1  12419  ennnfonelemim  12425  exmidunben  12427  ctiunctlemfo  12440  omiunct  12445  ssnnctlemct  12447  isstruct2r  12473  ismgm  12776  issgrp  12809  sgrpidmndm  12821  mndpropd  12841  issubmnd  12843  isgrpinv  12926  grplmulf1o  12944  dfgrp3mlem  12968  grplactcnv  12972  mhmid  12979  mhmmnd  12980  ghmgrp  12982  mulgval  12986  mulgfng  12987  mulgnnp1  12991  mulgnn0dir  13013  mulgneg2  13017  mhmmulg  13024  grpissubg  13054  isnsg  13062  isnsg3  13067  nmzsubg  13070  issrg  13148  srglmhm  13176  srgrmhm  13177  isring  13183  ringadd2  13210  oppr1g  13252  reldvdsrsrg  13261  dvdsrvald  13262  dvdsrd  13263  dvdsrex  13267  dvdsrmul1  13271  unitgrp  13285  subrgintm  13364  subrgpropd  13369  lmodprop2d  13438  opnssneib  13659  restbasg  13671  restopn2  13686  iscnp4  13721  cnss2  13730  cnconst2  13736  cnptopresti  13741  cnptoprest2  13743  neitx  13771  uptx  13777  txrest  13779  txdis1cn  13781  xmetres2  13882  xblss2ps  13907  blhalf  13911  blssps  13930  blss  13931  blssexps  13932  blssex  13933  blin2  13935  metequiv2  13999  bdmetval  14003  metcnp3  14014  metcnp  14015  metcn  14017  metcnpi  14018  metcnpi2  14019  txmetcnp  14021  txmetcn  14022  qtopbas  14025  tgqioo  14050  fsumcncntop  14059  elcncf2  14064  mulcncflem  14093  mulcncf  14094  suplociccreex  14105  limcdifap  14134  cnplimcim  14139  cnplimccntop  14142  limccnpcntop  14147  dvcj  14176  dveflem  14190  reeff1olem  14195  eflt  14199  sin0pilem1  14205  ptolemy  14248  coseq0q4123  14258  coseq0negpitopi  14260  cos02pilt1  14275  cos11  14277  ioocosf1o  14278  cxplt  14339  cxple  14340  cxplt3  14343  apcxp2  14361  rprelogbmul  14376  rprelogbdiv  14378  lgsval  14408  lgsfcl2  14410  lgscllem  14411  lgsval2lem  14414  lgsdir2lem4  14435  lgsdir2lem5  14436  lgsdir2  14437  lgsne0  14442  2sqlem6  14470  2sqlem10  14475  pwle2  14751  pwf1oexmid  14752  subctctexmid  14753  pw1nct  14755  peano4nninf  14758  nninfalllem1  14760  nninfall  14761  nninfsellemeq  14766  nninfsellemqall  14767  sbthom  14777  refeq  14779  isomninnlem  14781  trilpolemeq1  14791  trilpolemlt1  14792  trirec0  14795  apdiff  14799  iswomninnlem  14800  ismkvnnlem  14803  redcwlpolemeq1  14805  ltlenmkv  14820