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  1087  simp2lr  1091  simp3lr  1095  bilukdc  1440  dcun  3604  ifnefals  3650  intab  3957  exmid01  4288  exmidundif  4296  exmidundifim  4297  frirrg  4447  reg2exmidlema  4632  imadiflem  5409  fvco4  5718  fvmptt  5738  fcoconst  5818  funopsn  5829  f1imass  5914  fcof1  5923  fliftfun  5936  riotass2  5999  ovmpodxf  6146  dftpos4  6428  tfrlem1  6473  tfrlem3ag  6474  tfrlemibacc  6491  tfrlemibfn  6493  tfrlemi1  6497  tfrlemi14d  6498  tfr1onlem3ag  6502  tfr1onlembacc  6507  tfr1onlembfn  6509  tfr1onlemaccex  6513  tfrcllembacc  6520  tfrcllembfn  6522  tfrcllemaccex  6526  frecabcl  6564  nntr2  6670  dcdifsnid  6671  nnm00  6697  ecopovsymg  6802  ecopoverg  6804  th3qlem1  6805  mapss  6859  f1imaen2g  6966  pw2f1odclem  7019  xpen  7030  xpmapenlem  7034  phpm  7051  fidifsnen  7056  dif1enen  7068  fiunsnnn  7069  fin0  7073  fin0or  7074  findcard2d  7079  findcard2sd  7080  diffifi  7082  isinfinf  7085  tridc  7088  fimax2gtrilemstep  7089  fimax2gtri  7090  en2eqpr  7098  onunsnss  7108  unsnfidcex  7111  unsnfidcel  7112  undifdcss  7114  unfiin  7117  fisseneq  7126  ssfirab  7128  f1finf1o  7145  fidcenumlemrks  7151  fidcenumlemrk  7152  fidcenumlemr  7153  fidcenum  7154  suplub2ti  7199  supisolem  7206  ordiso2  7233  djudom  7291  omp1eomlem  7292  difinfsnlem  7297  difinfinf  7299  ctm  7307  ctssdclemn0  7308  enumct  7313  nnnninfeq  7326  nnnninfeq2  7327  nninfisol  7331  enomnilem  7336  finomni  7338  exmidomni  7340  fodju0  7345  ismkvnex  7353  enmkvlem  7359  enwomnilem  7367  pr2cv1  7399  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  exmidaclem  7422  exmidontriimlem1  7435  exmidontriimlem2  7436  exmidontriimlem3  7437  exmidontriimlem4  7438  exmidontriim  7439  netap  7472  exmidapne  7478  dfplpq2  7573  dfmpq2  7574  mulpipqqs  7592  nqpi  7597  distrnqg  7606  prarloclemarch  7637  enq0tr  7653  nqnq0pi  7657  nq0nn  7661  nnnq0lem1  7665  prarloclemup  7714  prarloclem3  7716  prarloclemcalc  7721  genplt2i  7729  addnqprllem  7746  addnqprulem  7747  appdivnq  7782  distrlem1prl  7801  distrlem1pru  7802  ltaddpr  7816  ltexprlemlol  7821  ltexprlemupu  7823  ltexprlemdisj  7825  addcanprleml  7833  ltaprlem  7837  addextpr  7840  recexprlemopu  7846  recexprlemdisj  7849  recexprlem1ssl  7852  aptiprleml  7858  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemopu  7867  cauappcvgprlemdisj  7870  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemopu  7890  caucvgprlemladdfu  7896  caucvgprprlemml  7913  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemopu  7918  caucvgprprlemexbt  7925  suplocexprlemru  7938  suplocexprlemloc  7940  suplocexprlemub  7942  suplocexprlemlub  7943  prsrlem1  7961  recexgt0sr  7992  mulgt0sr  7997  archsr  8001  caucvgsrlemcau  8012  caucvgsrlemoffcau  8017  caucvgsrlemoffres  8019  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  addcnsr  8053  mulcnsr  8054  mulcnsrec  8062  axmulcom  8090  nntopi  8113  axcaucvglemcau  8117  axcaucvglemres  8118  axpre-suploclemres  8120  axpre-suploc  8121  mpomulf  8168  axsuploc  8251  ltntri  8306  cnegexlem2  8354  cnegexlem3  8355  addsub4  8421  le2add  8623  lt2add  8624  lt2sub  8639  le2sub  8640  rereim  8765  apreim  8782  mulreim  8783  apcotr  8786  apadd1  8787  addext  8789  mulext1  8791  mulext  8793  apti  8801  aptap  8829  receuap  8848  rec11rap  8890  divdivdivap  8892  divadddivap  8906  divsubdivap  8907  rerecclap  8909  recgt0  9029  prodgt0gt0  9030  prodgt0  9031  prodge0  9033  lemulge11  9045  lt2mul2div  9058  ltrec  9062  lerec  9063  ltrec1  9067  lediv2a  9074  mulle0r  9123  sup3exmid  9136  zdiv  9567  eluzuzle  9763  supinfneg  9828  infsupneg  9829  infregelbex  9831  xrltso  10030  xnn0dcle  10036  xnn0letri  10037  npnflt  10049  nmnfgt  10052  z2ge  10060  xaddf  10078  xaddval  10079  xpncan  10105  xleadd1a  10107  xltadd1  10110  xaddge0  10112  xle2add  10113  xleaddadd  10121  ixxss1  10138  ixxss2  10139  elico2  10171  iccsupr  10200  fzass4  10296  fzrev  10318  fz0fzelfz0  10361  fzocatel  10443  elfzomelpfzo  10475  zsupcllemstep  10488  exbtwnzlemstep  10506  rebtwn2zlemstep  10511  qbtwnxr  10516  xqltnle  10526  apbtwnz  10533  btwnzge0  10559  modqid  10610  modqcyc  10620  modqcyc2  10621  modqaddabs  10623  modqaddmod  10624  mulqaddmodid  10625  modqmuladd  10627  modqltm1p1mod  10637  modqsubmod  10643  modqsubmodmod  10644  modaddmodlo  10649  modqmulmod  10650  modqmulmodr  10651  modqsubdir  10654  addmodlteq  10659  nninfinf  10704  iseqf1olemab  10763  iseqf1olemmo  10766  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  seqf1oglem1  10780  seqf1oglem2  10781  seqf1og  10782  exp3val  10802  expcl2lemap  10812  expap0  10830  expnegzap  10834  expmul  10845  leexp1a  10855  qsqeqor  10911  expnbnd  10924  nn0ltexp2  10970  nn0opth2  10985  facndiv  11000  faclbnd  11002  bcval5  11024  bcpasc  11027  hashennnuni  11040  hashunlem  11066  hashunsng  11070  hashprg  11071  fiprsshashgt1  11080  hashxp  11089  fimaxq  11090  zfz1isolemiso  11102  zfz1isolem1  11103  seq3coll  11105  iswrdiz  11119  wrdnval  11143  ccatlen  11171  ccatvalfn  11177  ccatsymb  11178  ccatalpha  11189  ccat2s1fstg  11224  swrdclg  11230  swrdsb0eq  11245  pfxwrdsymbg  11270  wrdind  11302  wrd2ind  11303  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12  11313  pfxccat3  11314  swrdccat  11315  shftlem  11376  shftfvalg  11378  shftfval  11381  2shfti  11391  caucvgrelemrec  11539  caucvgrelemcau  11540  caucvgre  11541  cvg1nlemcau  11544  cvg1nlemres  11545  resqrexlemcalc3  11576  resqrexlemcvg  11579  resqrexlemglsq  11582  resqrexlemga  11583  sqrtsq  11604  leabs  11634  absexpzap  11640  abslt  11648  absle  11649  abssubap0  11650  caubnd2  11677  icodiamlt  11740  maxleim  11765  maxabslemval  11768  maxleastlt  11775  rexico  11781  zmaxcl  11784  fimaxre2  11787  minmax  11790  xrmaxleim  11804  xrmaxiflemcl  11805  xrmaxifle  11806  xrmaxiflemlub  11808  xrmaxiflemval  11810  xrmaxleastlt  11816  xrmaxltsup  11818  xrmaxadd  11821  xrminmax  11825  xrbdtri  11836  climuni  11853  climshftlemg  11862  iserex  11899  climcau  11907  climrecvg1n  11908  climcvg1nlem  11909  sumeq2  11919  summodclem3  11940  zsumdc  11944  isumss  11951  fisumss  11952  sumsnf  11969  fsumconst  12014  modfsummod  12018  fsum00  12022  fsumabs  12025  fsumrelem  12031  fsumiun  12037  isumsplit  12051  divcnv  12057  geo2sum  12074  geoisumr  12078  cvgratz  12092  ntrivcvgap  12108  prodeq2  12117  prodmodclem2  12137  prodmodc  12138  zproddc  12139  fprodmul  12151  prodsnf  12152  fprodcl2lem  12165  fprodconst  12180  fprodap0  12181  fprodrec  12189  fprodap0f  12196  fprodle  12200  fprodmodd  12201  tanaddap  12299  zdvdsdc  12372  dvds2ln  12384  fsumdvds  12402  dvdsle  12404  dvdsext  12415  divalglemeunn  12481  divalglemex  12482  divalglemeuneg  12483  bitsfzo  12515  bitsmod  12516  bitsinv1lem  12521  bitsinv1  12522  dvdsbnd  12526  gcdsupex  12527  gcdsupcl  12528  dvdslegcd  12534  bezoutlemnewy  12566  bezoutlemstep  12567  bezoutlemmain  12568  bezoutlemzz  12572  bezoutlembz  12574  bezoutlembi  12575  bezoutlemle  12578  dfgcd3  12580  bezout  12581  dfgcd2  12584  dvdsmulgcd  12595  bezoutr  12602  uzwodc  12607  nninfctlemfo  12610  lcmval  12634  lcmcllem  12638  lcmneg  12645  ncoprmgcdne1b  12660  isprm2lem  12687  prmind2  12691  dvdsnprmd  12696  isprm5  12713  prmdvdsexp  12719  sqrt2irr  12733  oddpwdclemxy  12740  oddpwdclemdc  12744  nonsq  12778  pceu  12867  pcmul  12873  pc2dvds  12902  pcz  12904  pcprmpw2  12905  dvdsprmpweqle  12909  pcfac  12922  qexpz  12924  prmpwdvds  12927  1arith  12939  mul4sq  12966  4sqexercise2  12971  4sqlemsdc  12972  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemhom  13035  ennnfonelemfun  13037  ennnfonelemf1  13038  ennnfonelemim  13044  exmidunben  13046  ctiunctlemfo  13059  omiunct  13064  ssnnctlemct  13066  isstruct2r  13092  prdsval  13355  ismgm  13439  issgrp  13485  sgrppropd  13495  sgrpidmndm  13502  mndpropd  13522  issubmnd  13524  prdsidlem  13529  resmhm2b  13571  gsumwmhm  13580  isgrpinv  13636  grplmulf1o  13656  dfgrp3mlem  13680  grplactcnv  13684  pwssub  13695  mhmid  13701  mhmmnd  13702  ghmgrp  13704  mulgval  13708  mulgfng  13710  mulgnnp1  13716  mulgnn0dir  13738  mulgneg2  13742  mhmmulg  13749  grpissubg  13780  isnsg  13788  isnsg3  13793  nmzsubg  13796  ghmmhmb  13840  ghmpreima  13852  ghmnsgpreima  13855  ghmf1  13859  ghmf1o  13861  conjghm  13862  conjnmz  13865  conjnmzb  13866  ghmcmn  13913  gsumfzconst  13927  issrg  13977  srglmhm  14005  srgrmhm  14006  isring  14012  ringadd2  14039  ringlghm  14073  ringrghm  14074  oppr1g  14094  dvdsrvald  14106  dvdsrd  14107  dvdsrex  14111  dvdsrmul1  14115  unitgrp  14129  rhmopp  14189  subrgintm  14256  subrgpropd  14266  isdomn  14282  lmodprop2d  14361  lssvacl  14378  lssvsubcl  14379  lssvscl  14388  lsslss  14394  lss1d  14396  lsspropdg  14444  expghmap  14620  mulgghm2  14621  znunit  14672  znrrg  14673  mplvalcoe  14703  mplsubgfilemcl  14712  mplsubgfileminv  14713  mplsubgfi  14714  opnssneib  14879  restbasg  14891  restopn2  14906  iscnp4  14941  cnss2  14950  cnconst2  14956  cnptopresti  14961  cnptoprest2  14963  neitx  14991  uptx  14997  txrest  14999  txdis1cn  15001  xmetres2  15102  xblss2ps  15127  blhalf  15131  blssps  15150  blss  15151  blssexps  15152  blssex  15153  blin2  15155  metequiv2  15219  bdmetval  15223  metcnp3  15234  metcnp  15235  metcn  15237  metcnpi  15238  metcnpi2  15239  txmetcnp  15241  txmetcn  15242  qtopbas  15245  tgqioo  15278  mpomulcn  15289  fsumcncntop  15290  elcncf2  15297  mulcncflem  15330  mulcncf  15331  suplociccreex  15347  limcdifap  15385  cnplimcim  15390  cnplimccntop  15393  limccnpcntop  15398  dvcj  15432  dvmptfsum  15448  dveflem  15449  ply1termlem  15465  plyaddlem1  15470  plymullem1  15471  plycolemc  15481  plycjlemc  15483  plyrecj  15486  dvply1  15488  reeff1olem  15494  eflt  15498  sin0pilem1  15504  ptolemy  15547  coseq0q4123  15557  coseq0negpitopi  15559  cos02pilt1  15574  cos11  15576  ioocosf1o  15577  rpcxpmul2  15636  cxplt  15639  cxple  15640  cxplt3  15643  apcxp2  15662  rprelogbmul  15678  rprelogbdiv  15680  dvdsppwf1o  15712  perfect  15724  lgsval  15732  lgsfcl2  15734  lgscllem  15735  lgsval2lem  15738  lgsdir2lem4  15759  lgsdir2lem5  15760  lgsdir2  15761  lgsne0  15766  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  2sqlem6  15848  2sqlem10  15853  umgrnloopv  15964  umgrvad2edg  16061  usgr1eop  16095  wlkvtxiedg  16195  wlkvtxiedgg  16196  upgredginwlk  16206  upgriswlkdc  16210  clwwlkccatlem  16250  pw1ndom3  16589  2omap  16594  pw1map  16596  pwle2  16599  pwf1oexmid  16600  subctctexmid  16601  pw1nct  16604  peano4nninf  16608  nninfalllem1  16610  nninfall  16611  nninfsellemeq  16616  nninfsellemqall  16617  nnnninfex  16624  nninfnfiinf  16625  sbthom  16630  refeq  16632  isomninnlem  16634  trilpolemeq1  16644  trilpolemlt1  16645  trirec0  16648  apdiff  16652  iswomninnlem  16653  ismkvnnlem  16656  redcwlpolemeq1  16658  ltlenmkv  16674