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  7318  suplub2ti  7341  supisolem  7348  ordiso2  7375  djudom  7433  omp1eomlem  7434  difinfsnlem  7439  difinfinf  7441  ctm  7449  ctssdclemn0  7450  enumct  7455  nnnninfeq  7468  nnnninfeq2  7469  nninfisol  7473  enomnilem  7478  finomni  7480  exmidomni  7482  fodju0  7487  ismkvnex  7495  enmkvlem  7501  enwomnilem  7509  pr2cv1  7541  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  exmidontriimlem1  7577  exmidontriimlem2  7578  exmidontriimlem3  7579  exmidontriimlem4  7580  exmidontriim  7581  netap  7620  exmidapne  7626  dfplpq2  7721  dfmpq2  7722  mulpipqqs  7740  nqpi  7745  distrnqg  7754  prarloclemarch  7785  enq0tr  7801  nqnq0pi  7805  nq0nn  7809  nnnq0lem1  7813  prarloclemup  7862  prarloclem3  7864  prarloclemcalc  7869  genplt2i  7877  addnqprllem  7894  addnqprulem  7895  appdivnq  7930  distrlem1prl  7949  distrlem1pru  7950  ltaddpr  7964  ltexprlemlol  7969  ltexprlemupu  7971  ltexprlemdisj  7973  addcanprleml  7981  ltaprlem  7985  addextpr  7988  recexprlemopu  7994  recexprlemdisj  7997  recexprlem1ssl  8000  aptiprleml  8006  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemdisj  8018  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemladdfu  8044  caucvgprprlemml  8061  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemexbt  8073  suplocexprlemru  8086  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  prsrlem1  8109  recexgt0sr  8140  mulgt0sr  8145  archsr  8149  caucvgsrlemcau  8160  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  addcnsr  8201  mulcnsr  8202  mulcnsrec  8210  axmulcom  8238  nntopi  8261  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  mpomulf  8316  axsuploc  8398  ltntri  8454  cnegexlem2  8502  cnegexlem3  8503  addsub4  8569  le2add  8772  lt2add  8773  lt2sub  8788  le2sub  8789  rereim  8914  apreim  8931  mulreim  8932  apcotr  8935  apadd1  8936  addext  8938  mulext1  8940  mulext  8942  apti  8950  aptap  8978  receuap  8999  rec11rap  9041  divdivdivap  9043  divadddivap  9057  divsubdivap  9058  rerecclap  9060  recgt0  9180  prodgt0gt0  9181  prodgt0  9182  prodge0  9184  lemulge11  9196  lt2mul2div  9209  ltrec  9213  lerec  9214  ltrec1  9218  lediv2a  9225  mulle0r  9274  sup3exmid  9287  zdiv  9734  eluzuzle  9930  supinfneg  9995  infsupneg  9996  infregelbex  9998  xrltso  10198  xnn0dcle  10204  xnn0letri  10205  npnflt  10217  nmnfgt  10220  z2ge  10228  xaddf  10246  xaddval  10247  xpncan  10273  xleadd1a  10275  xltadd1  10278  xaddge0  10280  xle2add  10281  xleaddadd  10289  ixxss1  10306  ixxss2  10307  elico2  10339  iccsupr  10368  fzass4  10468  fzrev  10491  fz0fzelfz0  10534  fzocatel  10617  elfzomelpfzo  10649  zsupcllemstep  10662  exbtwnzlemstep  10682  rebtwn2zlemstep  10687  qbtwnxr  10692  xqltnle  10702  apbtwnz  10709  btwnzge0  10735  modqid  10786  modqcyc  10796  modqcyc2  10797  modqaddabs  10799  modqaddmod  10800  mulqaddmodid  10801  modqmuladd  10803  modqltm1p1mod  10813  modqsubmod  10819  modqsubmodmod  10820  modaddmodlo  10825  modqmulmod  10826  modqmulmodr  10827  modqsubdir  10830  addmodlteq  10835  nninfinf  10880  iseqf1olemab  10939  iseqf1olemmo  10942  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  seqf1oglem1  10956  seqf1oglem2  10957  seqf1og  10958  exp3val  10978  expcl2lemap  10988  expap0  11006  expnegzap  11010  expmul  11021  leexp1a  11031  qsqeqor  11087  resq01  11095  expnbnd  11101  nn0ltexp2  11147  nn0opth2  11162  facndiv  11177  faclbnd  11179  bcval5  11201  bcpasc  11204  hashennnuni  11218  hashunlem  11244  hashunsng  11248  hashprg  11249  fiprsshashgt1  11258  hashxp  11267  fimaxq  11270  hashfibc  11283  zfz1isolemiso  11291  zfz1isolem1  11292  seq3coll  11294  iswrdiz  11311  wrdnval  11335  ccatlen  11363  ccatvalfn  11369  ccatsymb  11370  ccatalpha  11381  ccat2s1fstg  11416  swrdclg  11422  swrdsb0eq  11437  pfxwrdsymbg  11462  wrdind  11494  wrd2ind  11495  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12  11505  pfxccat3  11506  swrdccat  11507  shftlem  11581  shftfvalg  11583  shftfval  11586  2shfti  11596  caucvgrelemrec  11745  caucvgrelemcau  11746  caucvgre  11747  cvg1nlemcau  11750  cvg1nlemres  11751  resqrexlemcalc3  11782  resqrexlemcvg  11785  resqrexlemglsq  11788  resqrexlemga  11789  sqrtsq  11810  leabs  11840  absexpzap  11846  abslt  11854  absle  11855  abssubap0  11856  caubnd2  11883  icodiamlt  11946  maxleim  11971  maxabslemval  11974  maxleastlt  11981  rexico  11987  zmaxcl  11990  fimaxre2  11993  minmax  11996  xrmaxleim  12010  xrmaxiflemcl  12011  xrmaxifle  12012  xrmaxiflemlub  12014  xrmaxiflemval  12016  xrmaxleastlt  12022  xrmaxltsup  12024  xrmaxadd  12027  xrminmax  12031  xrbdtri  12042  climuni  12059  climshftlemg  12068  iserex  12105  climcau  12113  climrecvg1n  12114  climcvg1nlem  12115  sumeq2  12125  summodclem3  12147  zsumdc  12151  isumss  12158  fisumss  12159  sumsnf  12176  fsumconst  12221  modfsummod  12225  fsum00  12229  fsumabs  12232  fsumrelem  12238  fsumiun  12244  isumsplit  12258  divcnv  12264  geo2sum  12281  geoisumr  12285  cvgratz  12299  ntrivcvgap  12315  prodeq2  12324  prodmodclem2  12344  prodmodc  12345  zproddc  12346  fprodmul  12358  prodsnf  12359  fprodcl2lem  12372  fprodconst  12387  fprodap0  12388  fprodrec  12396  fprodap0f  12403  fprodle  12407  fprodmodd  12408  tanaddap  12506  zdvdsdc  12579  dvds2ln  12591  fsumdvds  12609  dvdsle  12611  dvdsext  12622  divalglemeunn  12688  divalglemex  12689  divalglemeuneg  12690  bitsfzo  12722  bitsmod  12723  bitsinv1lem  12728  bitsinv1  12729  dvdsbnd  12733  gcdsupex  12734  gcdsupcl  12735  dvdslegcd  12741  bezoutlemnewy  12773  bezoutlemstep  12774  bezoutlemmain  12775  bezoutlemzz  12779  bezoutlembz  12781  bezoutlembi  12782  bezoutlemle  12785  dfgcd3  12787  bezout  12788  dfgcd2  12791  dvdsmulgcd  12802  bezoutr  12809  uzwodc  12814  nninfctlemfo  12817  lcmval  12841  lcmcllem  12845  lcmneg  12852  ncoprmgcdne1b  12867  isprm2lem  12894  prmind2  12898  dvdsnprmd  12903  isprm5  12920  prmdvdsexp  12926  sqrt2irr  12940  oddpwdclemxy  12947  oddpwdclemdc  12951  nonsq  12985  pceu  13074  pcmul  13080  pc2dvds  13109  pcz  13111  pcprmpw2  13112  dvdsprmpweqle  13116  pcfac  13129  qexpz  13131  prmpwdvds  13134  1arith  13146  mul4sq  13173  4sqexercise2  13178  4sqlemsdc  13179  ballotfilem2  13228  ballotfilemsle  13248  ballotfilemsdom  13255  ballotfilemsima  13259  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ennnfonelemhom  13306  ennnfonelemfun  13308  ennnfonelemf1  13309  ennnfonelemim  13315  exmidunben  13317  ctiunctlemfo  13330  omiunct  13335  ssnnctlemct  13337  isstruct2r  13363  ismgm  13677  issgrp  13718  sgrppropd  13728  sgrpidmndm  13733  mndpropd  13753  issubmnd  13755  resmhm2b  13796  gzsumwmhm  13803  isgrpinv  13859  grplmulf1o  13879  dfgrp3mlem  13903  grplactcnv  13907  mhmid  13918  mhmmnd  13919  ghmgrp  13921  mulgval  13925  mulgfng  13927  mulgnnp1  13933  mulgnn0dir  13955  mulgneg2  13959  mhmmulg  13966  grpissubg  13997  isnsg  14005  isnsg3  14010  nmzsubg  14013  ghmmhmb  14057  ghmpreima  14069  ghmnsgpreima  14072  ghmf1  14076  ghmf1o  14078  conjghm  14079  conjnmz  14082  conjnmzb  14083  ghmcmn  14131  gzsumconst  14143  gsumzfi  14158  gsumclfi  14159  gsummptfidmadd  14161  gsumsubmclfi  14163  gsumconstcmn  14166  prdsval  14173  prdsidlem  14193  pwssub  14216  issrg  14269  srglmhm  14297  srgrmhm  14298  isring  14304  ringadd2  14332  ringlghm  14366  ringrghm  14367  oppr1g  14388  dvdsrvald  14400  dvdsrd  14401  dvdsrex  14405  dvdsrmul1  14409  unitgrp  14423  rhmopp  14483  subrgintm  14551  subrgpropd  14561  isdomn  14578  aprnzr  14599  opprdrng  14620  lmodprop2d  14685  lssvacl  14702  lssvsubcl  14703  lssvscl  14712  lsslss  14718  lss1d  14720  lsspropdg  14768  gsumfsum  14923  expghmap  14942  mulgghm2  14943  znunit  14994  znrrg  14995  issubassa2  15035  assamulgscmlem1  15041  assamulgscmlem2  15042  mplvalcoe  15081  mplsubgfilemcl  15090  mplsubgfileminv  15091  mplsubgfi  15092  opnssneib  15257  restbasg  15269  restopn2  15284  iscnp4  15319  cnss2  15328  cnconst2  15334  cnptopresti  15339  cnptoprest2  15341  neitx  15369  uptx  15375  txrest  15377  txdis1cn  15379  xmetres2  15480  xblss2ps  15505  blhalf  15509  blssps  15528  blss  15529  blssexps  15530  blssex  15531  blin2  15533  metequiv2  15597  bdmetval  15601  metcnp3  15612  metcnp  15613  metcn  15615  metcnpi  15616  metcnpi2  15617  txmetcnp  15619  txmetcn  15620  qtopbas  15623  tgqioo  15656  mpomulcn  15667  fsumcncntop  15668  elcncf2  15675  mulcncflem  15708  mulcncf  15709  suplociccreex  15725  limcdifap  15763  cnplimcim  15768  cnplimccntop  15771  limccnpcntop  15776  dvcj  15810  dvmptfsum  15826  dveflem  15827  ply1termlem  15843  plyaddlem1  15848  plymullem1  15849  plycolemc  15859  plycjlemc  15861  plyrecj  15864  dvply1  15866  reeff1olem  15872  eflt  15876  sin0pilem1  15882  ptolemy  15925  coseq0q4123  15935  coseq0negpitopi  15937  cos02pilt1  15952  cos11  15954  ioocosf1o  15955  rpcxpmul2  16015  cxplt  16018  cxple  16019  cxplt3  16022  apcxp2  16041  rprelogbmul  16057  rprelogbdiv  16059  birthdaylem3  16089  pellexlem3  16093  dvdsppwf1o  16103  perfect  16115  lgsval  16123  lgsfcl2  16125  lgscllem  16126  lgsval2lem  16129  lgsdir2lem4  16150  lgsdir2lem5  16151  lgsdir2  16152  lgsne0  16157  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  2sqlem6  16239  2sqlem10  16244  umgrnloopv  16355  umgrvad2edg  16452  usgr1eop  16486  wlkvtxiedg  16586  wlkvtxiedgg  16587  upgredginwlk  16597  upgriswlkdc  16601  clwwlkccatlem  16641  eupth2lem3lem4fi  16714  pw1ndom3  17020  pw1map  17025  pwle2  17028  pwf1oexmid  17029  subctctexmid  17030  pw1nct  17033  stnot  17039  peano4nninf  17049  nninfalllem1  17051  nninfall  17052  nninfsellemeq  17057  nninfsellemqall  17058  nnnninfex  17065  nninfnfiinf  17066  sbthom  17071  refeq  17073  isomninnlem  17079  trilpolemeq1  17089  trilpolemlt1  17090  trirec0  17093  apdiff  17097  iswomninnlem  17099  ismkvnnlem  17102  redcwlpolemeq1  17104  ltlenmkv  17120