Theorem simplr 533

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 493	1 |- ( ( ( ph /\ ps ) /\ ch ) -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp1lr  1092  simp2lr  1096  simp3lr  1100  bilukdc  1445  dcun  3637  ifnefals  3685  ifeqeqxdc  3687  intab  3999  exmid01  4335  exmidundif  4343  exmidundifim  4344  frirrg  4495  reg2exmidlema  4681  imadiflem  5460  relndmfv  5728  fvco4  5777  fvmptt  5797  fcoconst  5879  funopsn  5891  f1imass  5980  fcof1  5989  fliftfun  6002  riotass2  6067  ovmpodxf  6214  fsuppeq  6487  fsuppeqg  6488  suppssdc  6500  suppssfvg  6503  dftpos4  6534  tfrlem1  6579  tfrlem3ag  6580  tfrlemibacc  6597  tfrlemibfn  6599  tfrlemi1  6603  tfrlemi14d  6604  tfr1onlem3ag  6608  tfr1onlembacc  6613  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfrcllembacc  6626  tfrcllembfn  6628  tfrcllemaccex  6632  frecabcl  6670  nntr2  6776  dcdifsnid  6777  nnm00  6803  ecopovsymg  6908  ecopoverg  6910  th3qlem1  6911  mapss  6973  f1imaen2g  7080  pw2f1odclem  7134  xpen  7145  xpmapenlem  7149  mapunen  7151  phpm  7167  fidifsnen  7172  dif1enen  7184  fiunsnnn  7185  fin0  7189  fin0or  7190  findcard2d  7195  findcard2sd  7196  diffifi  7198  isinfinf  7201  tridc  7204  fimax2gtrilemstep  7205  fimax2gtri  7206  en2eqpr  7214  onunsnss  7224  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  unfiin  7233  fisseneq  7242  ssfirab  7244  f1finf1o  7264  fidcenumlemrks  7270  fidcenumlemrk  7271  fidcenumlemr  7272  fidcenum  7273  ffsuppbi  7300  fdcf1  7316  f1setfi  7317  2omap  7319  suplub2ti  7342  supisolem  7349  ordiso2  7376  djudom  7434  omp1eomlem  7435  difinfsnlem  7440  difinfinf  7442  ctm  7450  ctssdclemn0  7451  enumct  7456  nnnninfeq  7469  nnnninfeq2  7470  nninfisol  7474  enomnilem  7479  finomni  7481  exmidomni  7483  fodju0  7488  ismkvnex  7496  enmkvlem  7502  enwomnilem  7510  pr2cv1  7542  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  exmidaclem  7565  exmidontriimlem1  7578  exmidontriimlem2  7579  exmidontriimlem3  7580  exmidontriimlem4  7581  exmidontriim  7582  netap  7621  exmidapne  7627  dfplpq2  7722  dfmpq2  7723  mulpipqqs  7741  nqpi  7746  distrnqg  7755  prarloclemarch  7786  enq0tr  7802  nqnq0pi  7806  nq0nn  7810  nnnq0lem1  7814  prarloclemup  7863  prarloclem3  7865  prarloclemcalc  7870  genplt2i  7878  addnqprllem  7895  addnqprulem  7896  appdivnq  7931  distrlem1prl  7950  distrlem1pru  7951  ltaddpr  7965  ltexprlemlol  7970  ltexprlemupu  7972  ltexprlemdisj  7974  addcanprleml  7982  ltaprlem  7986  addextpr  7989  recexprlemopu  7995  recexprlemdisj  7998  recexprlem1ssl  8001  aptiprleml  8007  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemdisj  8019  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemladdfu  8045  caucvgprprlemml  8062  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemexbt  8074  suplocexprlemru  8087  suplocexprlemloc  8089  suplocexprlemub  8091  suplocexprlemlub  8092  prsrlem1  8110  recexgt0sr  8141  mulgt0sr  8146  archsr  8150  caucvgsrlemcau  8161  caucvgsrlemoffcau  8166  caucvgsrlemoffres  8168  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  addcnsr  8202  mulcnsr  8203  mulcnsrec  8211  axmulcom  8239  nntopi  8262  axcaucvglemcau  8266  axcaucvglemres  8267  axpre-suploclemres  8269  axpre-suploc  8270  mpomulf  8317  axsuploc  8399  ltntri  8456  cnegexlem2  8504  cnegexlem3  8505  addsub4  8571  le2add  8774  lt2add  8775  lt2sub  8790  le2sub  8791  rereim  8917  apreim  8934  mulreim  8935  apcotr  8938  apadd1  8939  addext  8941  mulext1  8943  mulext  8945  apti  8953  aptap  8981  receuap  9002  rec11rap  9044  divdivdivap  9046  divadddivap  9060  divsubdivap  9061  rerecclap  9063  recgt0  9183  prodgt0gt0  9184  prodgt0  9185  prodge0  9187  lemulge11  9199  lt2mul2div  9212  ltrec  9216  lerec  9217  ltrec1  9221  lediv2a  9228  mulle0r  9277  sup3exmid  9290  zdiv  9739  eluzuzle  9940  supinfneg  10005  infsupneg  10006  infregelbex  10008  irraddap  10057  xrltso  10209  xnn0dcle  10215  xnn0letri  10216  npnflt  10228  nmnfgt  10231  z2ge  10239  xaddf  10257  xaddval  10258  xpncan  10284  xleadd1a  10286  xltadd1  10289  xaddge0  10291  xle2add  10292  xleaddadd  10300  ixxss1  10317  ixxss2  10318  elico2  10350  iccsupr  10379  fzass4  10479  fzrev  10502  fz0fzelfz0  10545  fzocatel  10628  elfzomelpfzo  10660  zsupcllemstep  10673  exbtwnzlemstep  10693  rebtwn2zlemstep  10698  qbtwnxr  10703  xqltnle  10713  apbtwnz  10720  flaplt  10733  btwnzge0  10750  modqid  10801  modqcyc  10811  modqcyc2  10812  modqaddabs  10814  modqaddmod  10815  mulqaddmodid  10816  modqmuladd  10818  modqltm1p1mod  10828  modqsubmod  10834  modqsubmodmod  10835  modaddmodlo  10840  modqmulmod  10841  modqmulmodr  10842  modqsubdir  10845  addmodlteq  10850  nninfinf  10895  iseqf1olemab  10954  iseqf1olemmo  10957  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  seqf1oglem1  10971  seqf1oglem2  10972  seqf1og  10973  exp3val  10993  expcl2lemap  11003  expap0  11021  expnegzap  11025  expmul  11036  leexp1a  11046  qsqeqor  11102  resq01  11110  expnbnd  11116  nn0ltexp2  11163  nn0opth2  11178  facndiv  11193  faclbnd  11195  bcval5  11217  bcpasc  11220  hashennnuni  11234  hashunlem  11260  hashunsng  11264  hashprg  11265  fiprsshashgt1  11274  hashxp  11283  fimaxq  11286  hashfibc  11299  zfz1isolemiso  11307  zfz1isolem1  11308  seq3coll  11310  iswrdiz  11327  wrdnval  11351  ccatlen  11379  ccatvalfn  11385  ccatsymb  11386  ccatalpha  11397  ccat2s1fstg  11432  swrdclg  11438  swrdsb0eq  11453  pfxwrdsymbg  11478  wrdind  11510  wrd2ind  11511  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12  11521  pfxccat3  11522  swrdccat  11523  shftlem  11597  shftfvalg  11599  shftfval  11602  2shfti  11612  caucvgrelemrec  11761  caucvgrelemcau  11762  caucvgre  11763  cvg1nlemcau  11766  cvg1nlemres  11767  resqrexlemcalc3  11798  resqrexlemcvg  11801  resqrexlemglsq  11804  resqrexlemga  11805  sqrtsq  11826  leabs  11856  absexpzap  11863  abslt  11871  absle  11872  abssubap0  11873  caubnd2  11900  icodiamlt  11963  maxleim  11988  maxabslemval  11991  maxleastlt  11998  rexico  12004  zmaxcl  12007  fimaxre2  12010  fiidxsupcl  12012  minmax  12014  zmincl  12023  xrmaxleim  12029  xrmaxiflemcl  12030  xrmaxifle  12031  xrmaxiflemlub  12033  xrmaxiflemval  12035  xrmaxleastlt  12041  xrmaxltsup  12043  xrmaxadd  12046  xrminmax  12050  xrbdtri  12061  climuni  12078  climshftlemg  12087  iserex  12124  climcau  12132  climrecvg1n  12133  climcvg1nlem  12134  sumeq2  12144  summodclem3  12166  zsumdc  12170  isumss  12177  fisumss  12178  sumsnf  12195  fsumconst  12240  modfsummod  12244  fsum00  12248  fsumabs  12251  fsumrelem  12257  fsumiun  12263  isumsplit  12277  divcnv  12283  geo2sum  12300  geoisumr  12304  cvgratz  12318  ntrivcvgap  12334  prodeq2  12343  prodmodclem2  12363  prodmodc  12364  zproddc  12365  fprodmul  12377  prodsnf  12378  fprodcl2lem  12391  fprodconst  12406  fprodap0  12407  fprodrec  12415  fprodap0f  12422  fprodle  12426  fprodmodd  12427  tanaddap  12525  zdvdsdc  12598  dvds2ln  12610  fsumdvds  12628  dvdsle  12630  dvdsext  12641  divalglemeunn  12707  divalglemex  12708  divalglemeuneg  12709  bitsfzo  12741  bitsmod  12742  bitsinv1lem  12747  bitsinv1  12748  dvdsbnd  12752  gcdsupex  12753  gcdsupcl  12754  dvdslegcd  12760  bezoutlemnewy  12792  bezoutlemstep  12793  bezoutlemmain  12794  bezoutlemzz  12798  bezoutlembz  12800  bezoutlembi  12801  bezoutlemle  12804  dfgcd3  12806  bezout  12807  dfgcd2  12810  dvdsmulgcd  12821  bezoutr  12828  uzwodc  12833  nninfctlemfo  12836  lcmval  12860  lcmcllem  12864  lcmneg  12871  ncoprmgcdne1b  12886  isprm2lem  12913  prmind2  12917  dvdsnprmd  12922  isprm5  12940  prmdvdsexp  12946  sqrt2irr  12960  nonsq  13006  sqrtrirr  13008  pceu  13097  pcmul  13103  pc2dvds  13132  pcz  13134  pcprmpw2  13135  dvdsprmpweqle  13139  pcfac  13152  qexpz  13154  prmpwdvds  13157  1arith  13169  mul4sq  13196  4sqexercise2  13201  4sqlemsdc  13202  ballotfilem2  13280  ballotfilemsle  13300  ballotfilemsdom  13307  ballotfilemsima  13311  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ennnfonelemhom  13358  ennnfonelemfun  13360  ennnfonelemf1  13361  ennnfonelemim  13367  exmidunben  13369  ctiunctlemfo  13382  omiunct  13387  ssnnctlemct  13389  isstruct2r  13415  ismgm  13730  issgrp  13771  sgrppropd  13781  sgrpidmndm  13786  mndpropd  13806  issubmnd  13808  resmhm2b  13849  gzsumwmhm  13856  isgrpinv  13912  grplmulf1o  13932  dfgrp3mlem  13956  grplactcnv  13960  mhmid  13971  mhmmnd  13972  ghmgrp  13974  mulgval  13978  mulgfng  13980  mulgnnp1  13986  mulgnn0dir  14008  mulgneg2  14012  mhmmulg  14019  grpissubg  14050  isnsg  14058  isnsg3  14063  nmzsubg  14066  ghmmhmb  14110  ghmpreima  14122  ghmnsgpreima  14125  ghmf1  14129  ghmf1o  14131  conjghm  14132  conjnmz  14135  conjnmzb  14136  resscntz  14160  cntzsubg  14165  cntrsubgnsg  14169  ghmcmn  14215  gzsumconst  14227  gsumzfi  14242  gsumclfi  14243  gsummptfidmadd  14245  gsumsubmclfi  14247  gsumconstcmn  14250  prdsval  14257  prdsidlem  14277  pwssub  14300  issrg  14353  srglmhm  14381  srgrmhm  14382  isring  14388  ringadd2  14416  ringlghm  14450  ringrghm  14451  oppr1g  14472  dvdsrvald  14484  dvdsrd  14485  dvdsrex  14489  dvdsrmul1  14493  unitgrp  14507  rhmopp  14567  subrgintm  14635  subrgpropd  14645  isdomn  14662  aprnzr  14683  opprdrng  14704  lmodprop2d  14769  lssvacl  14786  lssvsubcl  14787  lssvscl  14796  lsslss  14802  lss1d  14804  lsspropdg  14852  gsumfsum  15007  expghmap  15026  mulgghm2  15027  znunit  15078  znrrg  15079  issubassa2  15119  assamulgscmlem1  15125  assamulgscmlem2  15126  mplvalcoe  15172  mplsubgfilemcl  15181  mplsubgfileminv  15182  mplsubgfi  15183  opnssneib  15348  restbasg  15360  restopn2  15375  iscnp4  15410  cnss2  15419  cnconst2  15425  cnptopresti  15430  cnptoprest2  15432  neitx  15460  uptx  15466  txrest  15468  txdis1cn  15470  xmetres2  15571  xblss2ps  15596  blhalf  15600  blssps  15619  blss  15620  blssexps  15621  blssex  15622  blin2  15624  metequiv2  15688  bdmetval  15692  metcnp3  15703  metcnp  15704  metcn  15706  metcnpi  15707  metcnpi2  15708  txmetcnp  15710  txmetcn  15711  qtopbas  15714  tgqioo  15747  mpomulcn  15758  fsumcncntop  15759  elcncf2  15766  mulcncflem  15799  mulcncf  15800  suplociccreex  15816  limcdifap  15854  cnplimcim  15859  cnplimccntop  15862  limccnpcntop  15867  dvcj  15901  dvmptfsum  15917  dveflem  15918  ply1termlem  15934  plyaddlem1  15939  plymullem1  15940  plycolemc  15950  plycjlemc  15952  plyrecj  15955  dvply1  15957  reeff1olem  15963  eflt  15967  sin0pilem1  15974  ptolemy  16017  coseq0q4123  16027  coseq0negpitopi  16029  cos02pilt1  16044  cos11  16046  ioocosf1o  16047  logdivlt  16088  logdivle  16089  rpcxpmul2  16110  cxplt  16113  cxple  16114  cxplt3  16117  apcxp2  16136  rprelogbmul  16152  rprelogbdiv  16154  birthdaylem3  16188  pellexlem3  16192  ppiqltx  16242  dvdsppwf1o  16244  chtqub  16257  perfect  16262  bcmax  16266  bposlem3  16274  bpos  16281  lgsval  16289  lgsfcl2  16291  lgscllem  16292  lgsval2lem  16295  lgsdir2lem4  16316  lgsdir2lem5  16317  lgsdir2  16318  lgsne0  16323  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  2sqlem6  16405  2sqlem10  16410  umgrnloopv  16521  umgrvad2edg  16618  usgr1eop  16652  wlkvtxiedg  16752  wlkvtxiedgg  16753  upgredginwlk  16763  upgriswlkdc  16767  clwwlkccatlem  16807  eupth2lem3lem4fi  16880  pw1ndom3  17186  pw1map  17191  pwle2  17194  pwf1oexmid  17195  subctctexmid  17196  pw1nct  17199  stnot  17205  peano4nninf  17215  nninfalllem1  17217  nninfall  17218  nninfsellemeq  17223  nninfsellemqall  17224  nnnninfex  17231  nninfnfiinf  17232  sbthom  17237  refeq  17239  isomninnlem  17245  trilpolemeq1  17256  trilpolemlt1  17257  trirec0  17260  apdiff  17264  iswomninnlem  17266  ismkvnnlem  17269  redcwlpolemeq1  17271  ltlenmkv  17287