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  sn0disj  4127  exmid01  4337  exmidundif  4345  exmidundifim  4346  frirrg  4497  reg2exmidlema  4683  imadiflem  5463  relndmfv  5731  fvco4  5780  fvmptt  5800  fcoconst  5882  funopsn  5894  f1imass  5983  fcof1  5992  fliftfun  6005  riotass2  6070  ovmpodxf  6217  fsuppeq  6491  fsuppeqg  6492  suppssdc  6504  suppssfvg  6507  dftpos4  6539  tfrlem1  6584  tfrlem3ag  6585  tfrlemibacc  6602  tfrlemibfn  6604  tfrlemi1  6608  tfrlemi14d  6609  tfr1onlem3ag  6613  tfr1onlembacc  6618  tfr1onlembfn  6620  tfr1onlemaccex  6624  tfrcllembacc  6631  tfrcllembfn  6633  tfrcllemaccex  6637  frecabcl  6675  nntr2  6781  dcdifsnid  6782  nnm00  6808  ecopovsymg  6913  ecopoverg  6915  th3qlem1  6916  mapss  6979  f1imaen2g  7086  pw2f1odclem  7140  xpen  7151  xpmapenlem  7155  mapunen  7157  phpm  7173  fidifsnen  7178  dif1enen  7190  fiunsnnn  7191  fin0  7195  fin0or  7196  findcard2d  7201  findcard2sd  7202  diffifi  7204  isinfinf  7207  tridc  7210  fimax2gtrilemstep  7211  fimax2gtri  7212  en2eqpr  7220  onunsnss  7230  unsnfidcex  7233  unsnfidcel  7234  undifdcss  7236  unfiin  7239  fisseneq  7248  ssfirab  7250  f1finf1o  7271  fidcenumlemrks  7277  fidcenumlemrk  7278  fidcenumlemr  7279  fidcenum  7280  fdcf1  7321  f1setfi  7322  2omap  7324  suplub2ti  7347  supisolem  7354  ordiso2  7381  djudom  7439  omp1eomlem  7440  difinfsnlem  7445  difinfinf  7447  ctm  7455  ctssdclemn0  7456  enumct  7461  nnnninfeq  7474  nnnninfeq2  7475  nninfisol  7479  enomnilem  7484  finomni  7486  exmidomni  7488  fodju0  7493  ismkvnex  7501  enmkvlem  7507  enwomnilem  7515  pr2cv1  7547  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidaclem  7570  exmidontriimlem1  7583  exmidontriimlem2  7584  exmidontriimlem3  7585  exmidontriimlem4  7586  exmidontriim  7587  netap  7626  exmidapne  7632  dfplpq2  7727  dfmpq2  7728  mulpipqqs  7746  nqpi  7751  distrnqg  7760  prarloclemarch  7791  enq0tr  7807  nqnq0pi  7811  nq0nn  7815  nnnq0lem1  7819  prarloclemup  7868  prarloclem3  7870  prarloclemcalc  7875  genplt2i  7883  addnqprllem  7900  addnqprulem  7901  appdivnq  7936  distrlem1prl  7955  distrlem1pru  7956  ltaddpr  7970  ltexprlemlol  7975  ltexprlemupu  7977  ltexprlemdisj  7979  addcanprleml  7987  ltaprlem  7991  addextpr  7994  recexprlemopu  8000  recexprlemdisj  8003  recexprlem1ssl  8006  aptiprleml  8012  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemdisj  8024  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemladdfu  8050  caucvgprprlemml  8067  caucvgprprlemopl  8070  caucvgprprlemlol  8071  caucvgprprlemopu  8072  caucvgprprlemexbt  8079  suplocexprlemru  8092  suplocexprlemloc  8094  suplocexprlemub  8096  suplocexprlemlub  8097  prsrlem1  8115  recexgt0sr  8146  mulgt0sr  8151  archsr  8155  caucvgsrlemcau  8166  caucvgsrlemoffcau  8171  caucvgsrlemoffres  8173  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  addcnsr  8207  mulcnsr  8208  mulcnsrec  8216  axmulcom  8244  nntopi  8267  axcaucvglemcau  8271  axcaucvglemres  8272  axpre-suploclemres  8274  axpre-suploc  8275  mpomulf  8322  axsuploc  8404  ltntri  8461  cnegexlem2  8509  cnegexlem3  8510  addsub4  8576  le2add  8779  lt2add  8780  lt2sub  8795  le2sub  8796  rereim  8922  apreim  8939  mulreim  8940  apcotr  8943  apadd1  8944  addext  8946  mulext1  8948  mulext  8950  apti  8958  aptap  8986  receuap  9007  rec11rap  9049  divdivdivap  9051  divadddivap  9065  divsubdivap  9066  rerecclap  9068  recgt0  9188  prodgt0gt0  9189  prodgt0  9190  prodge0  9192  lemulge11  9204  lt2mul2div  9217  ltrec  9221  lerec  9222  ltrec1  9226  lediv2a  9233  mulle0r  9282  sup3exmid  9295  zdiv  9744  eluzuzle  9945  supinfneg  10010  infsupneg  10011  infregelbex  10013  irraddap  10062  xrltso  10214  xnn0dcle  10220  xnn0letri  10221  npnflt  10233  nmnfgt  10236  z2ge  10244  xaddf  10262  xaddval  10263  xpncan  10289  xleadd1a  10291  xltadd1  10294  xaddge0  10296  xle2add  10297  xleaddadd  10305  ixxss1  10322  ixxss2  10323  elico2  10355  iccsupr  10384  fzass4  10484  fzrev  10507  fz0fzelfz0  10550  fzocatel  10633  elfzomelpfzo  10665  zsupcllemstep  10678  exbtwnzlemstep  10698  rebtwn2zlemstep  10703  qbtwnxr  10708  xqltnle  10718  apbtwnz  10725  flaplt  10738  btwnzge0  10755  modqid  10806  modqcyc  10816  modqcyc2  10817  modqaddabs  10819  modqaddmod  10820  mulqaddmodid  10821  modqmuladd  10823  modqltm1p1mod  10833  modqsubmod  10839  modqsubmodmod  10840  modaddmodlo  10845  modqmulmod  10846  modqmulmodr  10847  modqsubdir  10850  addmodlteq  10855  nninfinf  10900  iseqf1olemab  10959  iseqf1olemmo  10962  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  seqf1oglem1  10976  seqf1oglem2  10977  seqf1og  10978  exp3val  10998  expcl2lemap  11008  expap0  11026  expnegzap  11030  expmul  11041  leexp1a  11051  qsqeqor  11107  resq01  11115  expnbnd  11121  nn0ltexp2  11168  nn0opth2  11183  facndiv  11198  faclbnd  11200  bcval5  11222  bcpasc  11225  hashennnuni  11239  hashunlem  11265  hashunsng  11269  hashprg  11270  fiprsshashgt1  11279  hashxp  11288  fimaxq  11291  hashfibc  11304  zfz1isolemiso  11312  zfz1isolem1  11313  seq3coll  11315  iswrdiz  11332  wrdnval  11356  ccatlen  11384  ccatvalfn  11390  ccatsymb  11391  ccatalpha  11402  ccat2s1fstg  11437  swrdclg  11443  swrdsb0eq  11458  pfxwrdsymbg  11483  wrdind  11515  wrd2ind  11516  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12  11526  pfxccat3  11527  swrdccat  11528  shftlem  11602  shftfvalg  11604  shftfval  11607  2shfti  11617  caucvgrelemrec  11766  caucvgrelemcau  11767  caucvgre  11768  cvg1nlemcau  11771  cvg1nlemres  11772  resqrexlemcalc3  11803  resqrexlemcvg  11806  resqrexlemglsq  11809  resqrexlemga  11810  sqrtsq  11831  leabs  11861  absexpzap  11868  abslt  11876  absle  11877  abssubap0  11878  caubnd2  11905  icodiamlt  11968  maxleim  11993  maxabslemval  11996  maxleastlt  12003  rexico  12009  zmaxcl  12012  fimaxre2  12015  fiidxsupcl  12017  minmax  12019  zmincl  12028  xrmaxleim  12034  xrmaxiflemcl  12035  xrmaxifle  12036  xrmaxiflemlub  12038  xrmaxiflemval  12040  xrmaxleastlt  12046  xrmaxltsup  12048  xrmaxadd  12051  xrminmax  12055  xrbdtri  12066  climuni  12083  climshftlemg  12092  iserex  12129  climcau  12137  climrecvg1n  12138  climcvg1nlem  12139  sumeq2  12149  summodclem3  12171  zsumdc  12175  isumss  12182  fisumss  12183  sumsnf  12200  fsumconst  12245  modfsummod  12249  fsum00  12253  fsumabs  12256  fsumrelem  12262  fsumiun  12268  isumsplit  12282  divcnv  12288  geo2sum  12305  geoisumr  12309  cvgratz  12323  ntrivcvgap  12339  prodeq2  12348  prodmodclem2  12368  prodmodc  12369  zproddc  12370  fprodmul  12382  prodsnf  12383  fprodcl2lem  12396  fprodconst  12411  fprodap0  12412  fprodrec  12420  fprodap0f  12427  fprodle  12431  fprodmodd  12432  tanaddap  12530  zdvdsdc  12603  dvds2ln  12615  fsumdvds  12633  dvdsle  12635  dvdsext  12646  divalglemeunn  12712  divalglemex  12713  divalglemeuneg  12714  bitsfzo  12746  bitsmod  12747  bitsinv1lem  12752  bitsinv1  12753  dvdsbnd  12757  gcdsupex  12758  gcdsupcl  12759  dvdslegcd  12765  bezoutlemnewy  12797  bezoutlemstep  12798  bezoutlemmain  12799  bezoutlemzz  12803  bezoutlembz  12805  bezoutlembi  12806  bezoutlemle  12809  dfgcd3  12811  bezout  12812  dfgcd2  12815  dvdsmulgcd  12826  bezoutr  12833  uzwodc  12838  nninfctlemfo  12841  lcmval  12865  lcmcllem  12869  lcmneg  12876  ncoprmgcdne1b  12891  isprm2lem  12918  prmind2  12922  dvdsnprmd  12927  isprm5  12945  prmdvdsexp  12951  sqrt2irr  12965  nonsq  13011  sqrtrirr  13013  pceu  13102  pcmul  13108  pc2dvds  13137  pcz  13139  pcprmpw2  13140  dvdsprmpweqle  13144  pcfac  13157  qexpz  13159  prmpwdvds  13162  1arith  13174  mul4sq  13201  4sqexercise2  13206  4sqlemsdc  13207  ballotfilem2  13285  ballotfilemsle  13305  ballotfilemsdom  13312  ballotfilemsima  13316  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ennnfonelemhom  13363  ennnfonelemfun  13365  ennnfonelemf1  13366  ennnfonelemim  13372  exmidunben  13374  ctiunctlemfo  13387  omiunct  13392  ssnnctlemct  13394  isstruct2r  13420  ismgm  13735  issgrp  13776  sgrppropd  13786  sgrpidmndm  13791  mndpropd  13811  issubmnd  13813  resmhm2b  13854  gzsumwmhm  13861  isgrpinv  13917  grplmulf1o  13937  dfgrp3mlem  13961  grplactcnv  13965  mhmid  13976  mhmmnd  13977  ghmgrp  13979  mulgval  13983  mulgfng  13985  mulgnnp1  13991  mulgnn0dir  14013  mulgneg2  14017  mhmmulg  14024  grpissubg  14055  isnsg  14063  isnsg3  14068  nmzsubg  14071  ghmmhmb  14115  ghmpreima  14127  ghmnsgpreima  14130  ghmf1  14134  ghmf1o  14136  conjghm  14137  conjnmz  14140  conjnmzb  14141  resscntz  14165  cntzsubg  14170  cntrsubgnsg  14174  ghmcmn  14220  gzsumconst  14232  gsumzfi  14247  gsumclfi  14248  gsummptfidmadd  14250  gsumsubmclfi  14252  gsummptfidmsplit  14253  gsumsnfdcmn  14256  gsumresfi  14262  gsumconstcmn  14265  gsum2dfilem2  14271  prdsval  14279  prdsidlem  14299  pwssub  14322  issrg  14375  srglmhm  14403  srgrmhm  14404  isring  14410  ringadd2  14438  ringlghm  14472  ringrghm  14473  oppr1g  14496  dvdsrvald  14508  dvdsrd  14509  dvdsrex  14513  dvdsrmul1  14517  unitgrp  14531  rhmopp  14591  subrgintm  14659  subrgpropd  14669  isdomn  14686  aprnzr  14707  opprdrng  14728  lmodprop2d  14793  lssvacl  14810  lssvsubcl  14811  lssvscl  14820  lsslss  14826  lss1d  14828  lsspropdg  14876  gsumfsum  15031  expghmap  15050  mulgghm2  15051  znunit  15102  znrrg  15103  issubassa2  15143  assamulgscmlem1  15149  assamulgscmlem2  15150  psrbagmaxlem1  15178  psrass1filem  15186  psrass1fi  15210  mvrffi  15218  mplvalg  15222  mplsubgfileminv  15233  mplsubgfi  15234  opnssneib  15399  restbasg  15411  restopn2  15426  iscnp4  15461  cnss2  15470  cnconst2  15476  cnptopresti  15481  cnptoprest2  15483  neitx  15511  uptx  15517  txrest  15519  txdis1cn  15521  xmetres2  15622  xblss2ps  15647  blhalf  15651  blssps  15670  blss  15671  blssexps  15672  blssex  15673  blin2  15675  metequiv2  15739  bdmetval  15743  metcnp3  15754  metcnp  15755  metcn  15757  metcnpi  15758  metcnpi2  15759  txmetcnp  15761  txmetcn  15762  qtopbas  15765  tgqioo  15798  mpomulcn  15809  fsumcncntop  15810  elcncf2  15817  mulcncflem  15850  mulcncf  15851  suplociccreex  15867  limcdifap  15905  cnplimcim  15910  cnplimccntop  15913  limccnpcntop  15918  dvcj  15952  dvmptfsum  15968  dveflem  15969  ply1termlem  15985  plyaddlem1  15990  plymullem1  15991  plycolemc  16001  plycjlemc  16003  plyrecj  16006  dvply1  16008  reeff1olem  16014  eflt  16018  sin0pilem1  16025  ptolemy  16068  coseq0q4123  16078  coseq0negpitopi  16080  cos02pilt1  16096  cos11  16098  ioocosf1o  16099  logdivlt  16141  logdivle  16142  rpcxpmul2  16163  rpcxpmul2z  16165  cxplt  16168  cxple  16169  cxplt3  16172  apcxp2  16191  rprelogbmul  16208  rprelogbdiv  16210  birthdaylem3  16244  pellexlem3  16248  ppiqltx  16298  dvdsppwf1o  16300  chtqub  16313  perfect  16318  bcmax  16322  bposlem3  16330  bpos  16337  lgsval  16345  lgsfcl2  16347  lgscllem  16348  lgsval2lem  16351  lgsdir2lem4  16372  lgsdir2lem5  16373  lgsdir2  16374  lgsne0  16379  gausslemma2dlem1a  16399  gausslemma2dlem1f1o  16401  2sqlem6  16461  2sqlem10  16466  umgrnloopv  16577  umgrvad2edg  16674  usgr1eop  16708  wlkvtxiedg  16808  wlkvtxiedgg  16809  upgredginwlk  16819  upgriswlkdc  16823  clwwlkccatlem  16863  eupth2lem3lem4fi  16936  pw1ndom3  17242  pw1map  17247  pwle2  17250  pwf1oexmid  17251  subctctexmid  17252  pw1nct  17255  stnot  17261  peano4nninf  17272  nninfalllem1  17274  nninfall  17275  nninfsellemeq  17280  nninfsellemqall  17281  nnnninfex  17288  nninfnfiinf  17289  sbthom  17294  refeq  17296  isomninnlem  17302  trilpolemeq1  17313  trilpolemlt1  17314  trirec0  17317  apdiff  17321  iswomninnlem  17323  ismkvnnlem  17326  redcwlpolemeq1  17328  ltlenmkv  17344