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  6538  tfrlem1  6583  tfrlem3ag  6584  tfrlemibacc  6601  tfrlemibfn  6603  tfrlemi1  6607  tfrlemi14d  6608  tfr1onlem3ag  6612  tfr1onlembacc  6617  tfr1onlembfn  6619  tfr1onlemaccex  6623  tfrcllembacc  6630  tfrcllembfn  6632  tfrcllemaccex  6636  frecabcl  6674  nntr2  6780  dcdifsnid  6781  nnm00  6807  ecopovsymg  6912  ecopoverg  6914  th3qlem1  6915  mapss  6977  f1imaen2g  7084  pw2f1odclem  7138  xpen  7149  xpmapenlem  7153  mapunen  7155  phpm  7171  fidifsnen  7176  dif1enen  7188  fiunsnnn  7189  fin0  7193  fin0or  7194  findcard2d  7199  findcard2sd  7200  diffifi  7202  isinfinf  7205  tridc  7208  fimax2gtrilemstep  7209  fimax2gtri  7210  en2eqpr  7218  onunsnss  7228  unsnfidcex  7231  unsnfidcel  7232  undifdcss  7234  unfiin  7237  fisseneq  7246  ssfirab  7248  f1finf1o  7269  fidcenumlemrks  7275  fidcenumlemrk  7276  fidcenumlemr  7277  fidcenum  7278  ffsuppbi  7305  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  9745  eluzuzle  9946  supinfneg  10011  infsupneg  10012  infregelbex  10014  irraddap  10063  xrltso  10215  xnn0dcle  10221  xnn0letri  10222  npnflt  10234  nmnfgt  10237  z2ge  10245  xaddf  10263  xaddval  10264  xpncan  10290  xleadd1a  10292  xltadd1  10295  xaddge0  10297  xle2add  10298  xleaddadd  10306  ixxss1  10323  ixxss2  10324  elico2  10356  iccsupr  10385  fzass4  10485  fzrev  10508  fz0fzelfz0  10551  fzocatel  10634  elfzomelpfzo  10666  zsupcllemstep  10679  exbtwnzlemstep  10699  rebtwn2zlemstep  10704  qbtwnxr  10709  xqltnle  10719  apbtwnz  10726  flaplt  10739  btwnzge0  10756  modqid  10807  modqcyc  10817  modqcyc2  10818  modqaddabs  10820  modqaddmod  10821  mulqaddmodid  10822  modqmuladd  10824  modqltm1p1mod  10834  modqsubmod  10840  modqsubmodmod  10841  modaddmodlo  10846  modqmulmod  10847  modqmulmodr  10848  modqsubdir  10851  addmodlteq  10856  nninfinf  10901  iseqf1olemab  10960  iseqf1olemmo  10963  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  seqf1oglem1  10977  seqf1oglem2  10978  seqf1og  10979  exp3val  10999  expcl2lemap  11009  expap0  11027  expnegzap  11031  expmul  11042  leexp1a  11052  qsqeqor  11108  resq01  11116  expnbnd  11122  nn0ltexp2  11169  nn0opth2  11184  facndiv  11199  faclbnd  11201  bcval5  11223  bcpasc  11226  hashennnuni  11240  hashunlem  11266  hashunsng  11270  hashprg  11271  fiprsshashgt1  11280  hashxp  11289  fimaxq  11292  hashfibc  11305  zfz1isolemiso  11313  zfz1isolem1  11314  seq3coll  11316  iswrdiz  11333  wrdnval  11357  ccatlen  11385  ccatvalfn  11391  ccatsymb  11392  ccatalpha  11403  ccat2s1fstg  11438  swrdclg  11444  swrdsb0eq  11459  pfxwrdsymbg  11484  wrdind  11516  wrd2ind  11517  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12  11527  pfxccat3  11528  swrdccat  11529  shftlem  11603  shftfvalg  11605  shftfval  11608  2shfti  11618  caucvgrelemrec  11767  caucvgrelemcau  11768  caucvgre  11769  cvg1nlemcau  11772  cvg1nlemres  11773  resqrexlemcalc3  11804  resqrexlemcvg  11807  resqrexlemglsq  11810  resqrexlemga  11811  sqrtsq  11832  leabs  11862  absexpzap  11869  abslt  11877  absle  11878  abssubap0  11879  caubnd2  11906  icodiamlt  11969  maxleim  11994  maxabslemval  11997  maxleastlt  12004  rexico  12010  zmaxcl  12013  fimaxre2  12016  fiidxsupcl  12018  minmax  12020  zmincl  12029  xrmaxleim  12035  xrmaxiflemcl  12036  xrmaxifle  12037  xrmaxiflemlub  12039  xrmaxiflemval  12041  xrmaxleastlt  12047  xrmaxltsup  12049  xrmaxadd  12052  xrminmax  12056  xrbdtri  12067  climuni  12084  climshftlemg  12093  iserex  12130  climcau  12138  climrecvg1n  12139  climcvg1nlem  12140  sumeq2  12150  summodclem3  12172  zsumdc  12176  isumss  12183  fisumss  12184  sumsnf  12201  fsumconst  12246  modfsummod  12250  fsum00  12254  fsumabs  12257  fsumrelem  12263  fsumiun  12269  isumsplit  12283  divcnv  12289  geo2sum  12306  geoisumr  12310  cvgratz  12324  ntrivcvgap  12340  prodeq2  12349  prodmodclem2  12369  prodmodc  12370  zproddc  12371  fprodmul  12383  prodsnf  12384  fprodcl2lem  12397  fprodconst  12412  fprodap0  12413  fprodrec  12421  fprodap0f  12428  fprodle  12432  fprodmodd  12433  tanaddap  12531  zdvdsdc  12604  dvds2ln  12616  fsumdvds  12634  dvdsle  12636  dvdsext  12647  divalglemeunn  12713  divalglemex  12714  divalglemeuneg  12715  bitsfzo  12747  bitsmod  12748  bitsinv1lem  12753  bitsinv1  12754  dvdsbnd  12758  gcdsupex  12759  gcdsupcl  12760  dvdslegcd  12766  bezoutlemnewy  12798  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlemzz  12804  bezoutlembz  12806  bezoutlembi  12807  bezoutlemle  12810  dfgcd3  12812  bezout  12813  dfgcd2  12816  dvdsmulgcd  12827  bezoutr  12834  uzwodc  12839  nninfctlemfo  12842  lcmval  12866  lcmcllem  12870  lcmneg  12877  ncoprmgcdne1b  12892  isprm2lem  12919  prmind2  12923  dvdsnprmd  12928  isprm5  12946  prmdvdsexp  12952  sqrt2irr  12966  nonsq  13012  sqrtrirr  13014  pceu  13103  pcmul  13109  pc2dvds  13138  pcz  13140  pcprmpw2  13141  dvdsprmpweqle  13145  pcfac  13158  qexpz  13160  prmpwdvds  13163  1arith  13175  mul4sq  13202  4sqexercise2  13207  4sqlemsdc  13208  ballotfilem2  13286  ballotfilemsle  13306  ballotfilemsdom  13313  ballotfilemsima  13317  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemhom  13364  ennnfonelemfun  13366  ennnfonelemf1  13367  ennnfonelemim  13373  exmidunben  13375  ctiunctlemfo  13388  omiunct  13393  ssnnctlemct  13395  isstruct2r  13421  ismgm  13736  issgrp  13777  sgrppropd  13787  sgrpidmndm  13792  mndpropd  13812  issubmnd  13814  resmhm2b  13855  gzsumwmhm  13862  isgrpinv  13918  grplmulf1o  13938  dfgrp3mlem  13962  grplactcnv  13966  mhmid  13977  mhmmnd  13978  ghmgrp  13980  mulgval  13984  mulgfng  13986  mulgnnp1  13992  mulgnn0dir  14014  mulgneg2  14018  mhmmulg  14025  grpissubg  14056  isnsg  14064  isnsg3  14069  nmzsubg  14072  ghmmhmb  14116  ghmpreima  14128  ghmnsgpreima  14131  ghmf1  14135  ghmf1o  14137  conjghm  14138  conjnmz  14141  conjnmzb  14142  resscntz  14166  cntzsubg  14171  cntrsubgnsg  14175  ghmcmn  14221  gzsumconst  14233  gsumzfi  14248  gsumclfi  14249  gsummptfidmadd  14251  gsumsubmclfi  14253  gsummptfidmsplit  14254  gsumsnfdcmn  14257  gsumresfi  14263  gsumconstcmn  14266  gsum2dfilem2  14272  prdsval  14280  prdsidlem  14300  pwssub  14323  issrg  14376  srglmhm  14404  srgrmhm  14405  isring  14411  ringadd2  14439  ringlghm  14473  ringrghm  14474  oppr1g  14497  dvdsrvald  14509  dvdsrd  14510  dvdsrex  14514  dvdsrmul1  14518  unitgrp  14532  rhmopp  14592  subrgintm  14660  subrgpropd  14670  isdomn  14687  aprnzr  14708  opprdrng  14729  lmodprop2d  14794  lssvacl  14811  lssvsubcl  14812  lssvscl  14821  lsslss  14827  lss1d  14829  lsspropdg  14877  gsumfsum  15032  expghmap  15051  mulgghm2  15052  znunit  15103  znrrg  15104  issubassa2  15144  assamulgscmlem1  15150  assamulgscmlem2  15151  psrass1filem  15177  psrass1fi  15201  mplvalcoe  15206  mplsubgfilemcl  15215  mplsubgfileminv  15216  mplsubgfi  15217  opnssneib  15382  restbasg  15394  restopn2  15409  iscnp4  15444  cnss2  15453  cnconst2  15459  cnptopresti  15464  cnptoprest2  15466  neitx  15494  uptx  15500  txrest  15502  txdis1cn  15504  xmetres2  15605  xblss2ps  15630  blhalf  15634  blssps  15653  blss  15654  blssexps  15655  blssex  15656  blin2  15658  metequiv2  15722  bdmetval  15726  metcnp3  15737  metcnp  15738  metcn  15740  metcnpi  15741  metcnpi2  15742  txmetcnp  15744  txmetcn  15745  qtopbas  15748  tgqioo  15781  mpomulcn  15792  fsumcncntop  15793  elcncf2  15800  mulcncflem  15833  mulcncf  15834  suplociccreex  15850  limcdifap  15888  cnplimcim  15893  cnplimccntop  15896  limccnpcntop  15901  dvcj  15935  dvmptfsum  15951  dveflem  15952  ply1termlem  15968  plyaddlem1  15973  plymullem1  15974  plycolemc  15984  plycjlemc  15986  plyrecj  15989  dvply1  15991  reeff1olem  15997  eflt  16001  sin0pilem1  16008  ptolemy  16051  coseq0q4123  16061  coseq0negpitopi  16063  cos02pilt1  16079  cos11  16081  ioocosf1o  16082  logdivlt  16124  logdivle  16125  rpcxpmul2  16146  rpcxpmul2z  16148  cxplt  16151  cxple  16152  cxplt3  16155  apcxp2  16174  rprelogbmul  16191  rprelogbdiv  16193  birthdaylem3  16227  pellexlem3  16231  ppiqltx  16281  dvdsppwf1o  16283  chtqub  16296  perfect  16301  bcmax  16305  bposlem3  16313  bpos  16320  lgsval  16328  lgsfcl2  16330  lgscllem  16331  lgsval2lem  16334  lgsdir2lem4  16355  lgsdir2lem5  16356  lgsdir2  16357  lgsne0  16362  gausslemma2dlem1a  16382  gausslemma2dlem1f1o  16384  2sqlem6  16444  2sqlem10  16449  umgrnloopv  16560  umgrvad2edg  16657  usgr1eop  16691  wlkvtxiedg  16791  wlkvtxiedgg  16792  upgredginwlk  16802  upgriswlkdc  16806  clwwlkccatlem  16846  eupth2lem3lem4fi  16919  pw1ndom3  17225  pw1map  17230  pwle2  17233  pwf1oexmid  17234  subctctexmid  17235  pw1nct  17238  stnot  17244  peano4nninf  17255  nninfalllem1  17257  nninfall  17258  nninfsellemeq  17263  nninfsellemqall  17264  nnnninfex  17271  nninfnfiinf  17272  sbthom  17277  refeq  17279  isomninnlem  17285  trilpolemeq1  17296  trilpolemlt1  17297  trirec0  17300  apdiff  17304  iswomninnlem  17306  ismkvnnlem  17309  redcwlpolemeq1  17311  ltlenmkv  17327