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  1088  simp2lr  1092  simp3lr  1096  bilukdc  1441  dcun  3623  ifnefals  3671  ifeqeqxdc  3673  intab  3983  exmid01  4316  exmidundif  4324  exmidundifim  4325  frirrg  4476  reg2exmidlema  4661  imadiflem  5440  fvco4  5754  fvmptt  5774  fcoconst  5853  funopsn  5865  f1imass  5953  fcof1  5962  fliftfun  5975  riotass2  6040  ovmpodxf  6187  fsuppeq  6460  fsuppeqg  6461  suppssdc  6473  suppssfvg  6476  dftpos4  6507  tfrlem1  6552  tfrlem3ag  6553  tfrlemibacc  6570  tfrlemibfn  6572  tfrlemi1  6576  tfrlemi14d  6577  tfr1onlem3ag  6581  tfr1onlembacc  6586  tfr1onlembfn  6588  tfr1onlemaccex  6592  tfrcllembacc  6599  tfrcllembfn  6601  tfrcllemaccex  6605  frecabcl  6643  nntr2  6749  dcdifsnid  6750  nnm00  6776  ecopovsymg  6881  ecopoverg  6883  th3qlem1  6884  mapss  6939  f1imaen2g  7046  pw2f1odclem  7100  xpen  7111  xpmapenlem  7115  mapunen  7117  phpm  7133  fidifsnen  7138  dif1enen  7150  fiunsnnn  7151  fin0  7155  fin0or  7156  findcard2d  7161  findcard2sd  7162  diffifi  7164  isinfinf  7167  tridc  7170  fimax2gtrilemstep  7171  fimax2gtri  7172  en2eqpr  7180  onunsnss  7190  unsnfidcex  7193  unsnfidcel  7194  undifdcss  7196  unfiin  7199  fisseneq  7208  ssfirab  7210  f1finf1o  7230  fidcenumlemrks  7236  fidcenumlemrk  7237  fidcenumlemr  7238  fidcenum  7239  ffsuppbi  7266  2omap  7282  suplub2ti  7305  supisolem  7312  ordiso2  7339  djudom  7397  omp1eomlem  7398  difinfsnlem  7403  difinfinf  7405  ctm  7413  ctssdclemn0  7414  enumct  7419  nnnninfeq  7432  nnnninfeq2  7433  nninfisol  7437  enomnilem  7442  finomni  7444  exmidomni  7446  fodju0  7451  ismkvnex  7459  enmkvlem  7465  enwomnilem  7473  pr2cv1  7505  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  exmidontriimlem1  7541  exmidontriimlem2  7542  exmidontriimlem3  7543  exmidontriimlem4  7544  exmidontriim  7545  netap  7584  exmidapne  7590  dfplpq2  7685  dfmpq2  7686  mulpipqqs  7704  nqpi  7709  distrnqg  7718  prarloclemarch  7749  enq0tr  7765  nqnq0pi  7769  nq0nn  7773  nnnq0lem1  7777  prarloclemup  7826  prarloclem3  7828  prarloclemcalc  7833  genplt2i  7841  addnqprllem  7858  addnqprulem  7859  appdivnq  7894  distrlem1prl  7913  distrlem1pru  7914  ltaddpr  7928  ltexprlemlol  7933  ltexprlemupu  7935  ltexprlemdisj  7937  addcanprleml  7945  ltaprlem  7949  addextpr  7952  recexprlemopu  7958  recexprlemdisj  7961  recexprlem1ssl  7964  aptiprleml  7970  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemdisj  7982  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemladdfu  8008  caucvgprprlemml  8025  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemexbt  8037  suplocexprlemru  8050  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexprlemlub  8055  prsrlem1  8073  recexgt0sr  8104  mulgt0sr  8109  archsr  8113  caucvgsrlemcau  8124  caucvgsrlemoffcau  8129  caucvgsrlemoffres  8131  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  addcnsr  8165  mulcnsr  8166  mulcnsrec  8174  axmulcom  8202  nntopi  8225  axcaucvglemcau  8229  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  mpomulf  8280  axsuploc  8362  ltntri  8417  cnegexlem2  8465  cnegexlem3  8466  addsub4  8532  le2add  8735  lt2add  8736  lt2sub  8751  le2sub  8752  rereim  8877  apreim  8894  mulreim  8895  apcotr  8898  apadd1  8899  addext  8901  mulext1  8903  mulext  8905  apti  8913  aptap  8941  receuap  8960  rec11rap  9002  divdivdivap  9004  divadddivap  9018  divsubdivap  9019  rerecclap  9021  recgt0  9141  prodgt0gt0  9142  prodgt0  9143  prodge0  9145  lemulge11  9157  lt2mul2div  9170  ltrec  9174  lerec  9175  ltrec1  9179  lediv2a  9186  mulle0r  9235  sup3exmid  9248  zdiv  9684  eluzuzle  9880  supinfneg  9945  infsupneg  9946  infregelbex  9948  xrltso  10148  xnn0dcle  10154  xnn0letri  10155  npnflt  10167  nmnfgt  10170  z2ge  10178  xaddf  10196  xaddval  10197  xpncan  10223  xleadd1a  10225  xltadd1  10228  xaddge0  10230  xle2add  10231  xleaddadd  10239  ixxss1  10256  ixxss2  10257  elico2  10289  iccsupr  10318  fzass4  10417  fzrev  10440  fz0fzelfz0  10483  fzocatel  10566  elfzomelpfzo  10598  zsupcllemstep  10611  exbtwnzlemstep  10631  rebtwn2zlemstep  10636  qbtwnxr  10641  xqltnle  10651  apbtwnz  10658  btwnzge0  10684  modqid  10735  modqcyc  10745  modqcyc2  10746  modqaddabs  10748  modqaddmod  10749  mulqaddmodid  10750  modqmuladd  10752  modqltm1p1mod  10762  modqsubmod  10768  modqsubmodmod  10769  modaddmodlo  10774  modqmulmod  10775  modqmulmodr  10776  modqsubdir  10779  addmodlteq  10784  nninfinf  10829  iseqf1olemab  10888  iseqf1olemmo  10891  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  seqf1oglem1  10905  seqf1oglem2  10906  seqf1og  10907  exp3val  10927  expcl2lemap  10937  expap0  10955  expnegzap  10959  expmul  10970  leexp1a  10980  qsqeqor  11036  resq01  11044  expnbnd  11050  nn0ltexp2  11096  nn0opth2  11111  facndiv  11126  faclbnd  11128  bcval5  11150  bcpasc  11153  hashennnuni  11167  hashunlem  11193  hashunsng  11197  hashprg  11198  fiprsshashgt1  11207  hashxp  11216  fimaxq  11219  hashfibc  11232  zfz1isolemiso  11236  zfz1isolem1  11237  seq3coll  11239  iswrdiz  11256  wrdnval  11280  ccatlen  11308  ccatvalfn  11314  ccatsymb  11315  ccatalpha  11326  ccat2s1fstg  11361  swrdclg  11367  swrdsb0eq  11382  pfxwrdsymbg  11407  wrdind  11439  wrd2ind  11440  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12  11450  pfxccat3  11451  swrdccat  11452  shftlem  11526  shftfvalg  11528  shftfval  11531  2shfti  11541  caucvgrelemrec  11689  caucvgrelemcau  11690  caucvgre  11691  cvg1nlemcau  11694  cvg1nlemres  11695  resqrexlemcalc3  11726  resqrexlemcvg  11729  resqrexlemglsq  11732  resqrexlemga  11733  sqrtsq  11754  leabs  11784  absexpzap  11790  abslt  11798  absle  11799  abssubap0  11800  caubnd2  11827  icodiamlt  11890  maxleim  11915  maxabslemval  11918  maxleastlt  11925  rexico  11931  zmaxcl  11934  fimaxre2  11937  minmax  11940  xrmaxleim  11954  xrmaxiflemcl  11955  xrmaxifle  11956  xrmaxiflemlub  11958  xrmaxiflemval  11960  xrmaxleastlt  11966  xrmaxltsup  11968  xrmaxadd  11971  xrminmax  11975  xrbdtri  11986  climuni  12003  climshftlemg  12012  iserex  12049  climcau  12057  climrecvg1n  12058  climcvg1nlem  12059  sumeq2  12069  summodclem3  12091  zsumdc  12095  isumss  12102  fisumss  12103  sumsnf  12120  fsumconst  12165  modfsummod  12169  fsum00  12173  fsumabs  12176  fsumrelem  12182  fsumiun  12188  isumsplit  12202  divcnv  12208  geo2sum  12225  geoisumr  12229  cvgratz  12243  ntrivcvgap  12259  prodeq2  12268  prodmodclem2  12288  prodmodc  12289  zproddc  12290  fprodmul  12302  prodsnf  12303  fprodcl2lem  12316  fprodconst  12331  fprodap0  12332  fprodrec  12340  fprodap0f  12347  fprodle  12351  fprodmodd  12352  tanaddap  12450  zdvdsdc  12523  dvds2ln  12535  fsumdvds  12553  dvdsle  12555  dvdsext  12566  divalglemeunn  12632  divalglemex  12633  divalglemeuneg  12634  bitsfzo  12666  bitsmod  12667  bitsinv1lem  12672  bitsinv1  12673  dvdsbnd  12677  gcdsupex  12678  gcdsupcl  12679  dvdslegcd  12685  bezoutlemnewy  12717  bezoutlemstep  12718  bezoutlemmain  12719  bezoutlemzz  12723  bezoutlembz  12725  bezoutlembi  12726  bezoutlemle  12729  dfgcd3  12731  bezout  12732  dfgcd2  12735  dvdsmulgcd  12746  bezoutr  12753  uzwodc  12758  nninfctlemfo  12761  lcmval  12785  lcmcllem  12789  lcmneg  12796  ncoprmgcdne1b  12811  isprm2lem  12838  prmind2  12842  dvdsnprmd  12847  isprm5  12864  prmdvdsexp  12870  sqrt2irr  12884  oddpwdclemxy  12891  oddpwdclemdc  12895  nonsq  12929  pceu  13018  pcmul  13024  pc2dvds  13053  pcz  13055  pcprmpw2  13056  dvdsprmpweqle  13060  pcfac  13073  qexpz  13075  prmpwdvds  13078  1arith  13090  mul4sq  13117  4sqexercise2  13122  4sqlemsdc  13123  ballotfilem2  13172  ballotfilemsle  13192  ballotfilemsdom  13199  ballotfilemsima  13203  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemhom  13250  ennnfonelemfun  13252  ennnfonelemf1  13253  ennnfonelemim  13259  exmidunben  13261  ctiunctlemfo  13274  omiunct  13279  ssnnctlemct  13281  isstruct2r  13307  ismgm  13620  issgrp  13666  sgrppropd  13676  sgrpidmndm  13681  mndpropd  13701  issubmnd  13703  resmhm2b  13744  gsumwmhm  13753  isgrpinv  13809  grplmulf1o  13829  dfgrp3mlem  13853  grplactcnv  13857  mhmid  13868  mhmmnd  13869  ghmgrp  13871  mulgval  13875  mulgfng  13877  mulgnnp1  13883  mulgnn0dir  13905  mulgneg2  13909  mhmmulg  13916  grpissubg  13947  isnsg  13955  isnsg3  13960  nmzsubg  13963  ghmmhmb  14007  ghmpreima  14019  ghmnsgpreima  14022  ghmf1  14026  ghmf1o  14028  conjghm  14029  conjnmz  14032  conjnmzb  14033  ghmcmn  14080  gsumfzconst  14094  gfsumz  14109  gfsumcl  14110  prdsval  14115  prdsidlem  14135  pwssub  14158  issrg  14208  srglmhm  14236  srgrmhm  14237  isring  14243  ringadd2  14270  ringlghm  14304  ringrghm  14305  oppr1g  14326  dvdsrvald  14338  dvdsrd  14339  dvdsrex  14343  dvdsrmul1  14347  unitgrp  14361  rhmopp  14421  subrgintm  14489  subrgpropd  14499  isdomn  14516  aprnzr  14537  opprdrng  14558  lmodprop2d  14622  lssvacl  14639  lssvsubcl  14640  lssvscl  14649  lsslss  14655  lss1d  14657  lsspropdg  14705  expghmap  14881  mulgghm2  14882  znunit  14933  znrrg  14934  mplvalcoe  14971  mplsubgfilemcl  14980  mplsubgfileminv  14981  mplsubgfi  14982  opnssneib  15147  restbasg  15159  restopn2  15174  iscnp4  15209  cnss2  15218  cnconst2  15224  cnptopresti  15229  cnptoprest2  15231  neitx  15259  uptx  15265  txrest  15267  txdis1cn  15269  xmetres2  15370  xblss2ps  15395  blhalf  15399  blssps  15418  blss  15419  blssexps  15420  blssex  15421  blin2  15423  metequiv2  15487  bdmetval  15491  metcnp3  15502  metcnp  15503  metcn  15505  metcnpi  15506  metcnpi2  15507  txmetcnp  15509  txmetcn  15510  qtopbas  15513  tgqioo  15546  mpomulcn  15557  fsumcncntop  15558  elcncf2  15565  mulcncflem  15598  mulcncf  15599  suplociccreex  15615  limcdifap  15653  cnplimcim  15658  cnplimccntop  15661  limccnpcntop  15666  dvcj  15700  dvmptfsum  15716  dveflem  15717  ply1termlem  15733  plyaddlem1  15738  plymullem1  15739  plycolemc  15749  plycjlemc  15751  plyrecj  15754  dvply1  15756  reeff1olem  15762  eflt  15766  sin0pilem1  15772  ptolemy  15815  coseq0q4123  15825  coseq0negpitopi  15827  cos02pilt1  15842  cos11  15844  ioocosf1o  15845  rpcxpmul2  15904  cxplt  15907  cxple  15908  cxplt3  15911  apcxp2  15930  rprelogbmul  15946  rprelogbdiv  15948  pellexlem3  15973  dvdsppwf1o  15983  perfect  15995  lgsval  16003  lgsfcl2  16005  lgscllem  16006  lgsval2lem  16009  lgsdir2lem4  16030  lgsdir2lem5  16031  lgsdir2  16032  lgsne0  16037  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  2sqlem6  16119  2sqlem10  16124  umgrnloopv  16235  umgrvad2edg  16332  usgr1eop  16366  wlkvtxiedg  16466  wlkvtxiedgg  16467  upgredginwlk  16477  upgriswlkdc  16481  clwwlkccatlem  16521  eupth2lem3lem4fi  16594  pw1ndom3  16890  pw1map  16895  pwle2  16898  pwf1oexmid  16899  subctctexmid  16900  pw1nct  16903  peano4nninf  16910  nninfalllem1  16912  nninfall  16913  nninfsellemeq  16918  nninfsellemqall  16919  nnnninfex  16926  nninfnfiinf  16927  sbthom  16932  refeq  16934  isomninnlem  16940  trilpolemeq1  16950  trilpolemlt1  16951  trirec0  16954  apdiff  16958  iswomninnlem  16960  ismkvnnlem  16963  redcwlpolemeq1  16965  trimul0or  16971  ltlenmkv  16982