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  8455  cnegexlem2  8503  cnegexlem3  8504  addsub4  8570  le2add  8773  lt2add  8774  lt2sub  8789  le2sub  8790  rereim  8916  apreim  8933  mulreim  8934  apcotr  8937  apadd1  8938  addext  8940  mulext1  8942  mulext  8944  apti  8952  aptap  8980  receuap  9001  rec11rap  9043  divdivdivap  9045  divadddivap  9059  divsubdivap  9060  rerecclap  9062  recgt0  9182  prodgt0gt0  9183  prodgt0  9184  prodge0  9186  lemulge11  9198  lt2mul2div  9211  ltrec  9215  lerec  9216  ltrec1  9220  lediv2a  9227  mulle0r  9276  sup3exmid  9289  zdiv  9738  eluzuzle  9939  supinfneg  10004  infsupneg  10005  infregelbex  10007  irraddap  10056  xrltso  10208  xnn0dcle  10214  xnn0letri  10215  npnflt  10227  nmnfgt  10230  z2ge  10238  xaddf  10256  xaddval  10257  xpncan  10283  xleadd1a  10285  xltadd1  10288  xaddge0  10290  xle2add  10291  xleaddadd  10299  ixxss1  10316  ixxss2  10317  elico2  10349  iccsupr  10378  fzass4  10478  fzrev  10501  fz0fzelfz0  10544  fzocatel  10627  elfzomelpfzo  10659  zsupcllemstep  10672  exbtwnzlemstep  10692  rebtwn2zlemstep  10697  qbtwnxr  10702  xqltnle  10712  apbtwnz  10719  btwnzge0  10748  modqid  10799  modqcyc  10809  modqcyc2  10810  modqaddabs  10812  modqaddmod  10813  mulqaddmodid  10814  modqmuladd  10816  modqltm1p1mod  10826  modqsubmod  10832  modqsubmodmod  10833  modaddmodlo  10838  modqmulmod  10839  modqmulmodr  10840  modqsubdir  10843  addmodlteq  10848  nninfinf  10893  iseqf1olemab  10952  iseqf1olemmo  10955  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  seqf1oglem1  10969  seqf1oglem2  10970  seqf1og  10971  exp3val  10991  expcl2lemap  11001  expap0  11019  expnegzap  11023  expmul  11034  leexp1a  11044  qsqeqor  11100  resq01  11108  expnbnd  11114  nn0ltexp2  11161  nn0opth2  11176  facndiv  11191  faclbnd  11193  bcval5  11215  bcpasc  11218  hashennnuni  11232  hashunlem  11258  hashunsng  11262  hashprg  11263  fiprsshashgt1  11272  hashxp  11281  fimaxq  11284  hashfibc  11297  zfz1isolemiso  11305  zfz1isolem1  11306  seq3coll  11308  iswrdiz  11325  wrdnval  11349  ccatlen  11377  ccatvalfn  11383  ccatsymb  11384  ccatalpha  11395  ccat2s1fstg  11430  swrdclg  11436  swrdsb0eq  11451  pfxwrdsymbg  11476  wrdind  11508  wrd2ind  11509  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatin12  11519  pfxccat3  11520  swrdccat  11521  shftlem  11595  shftfvalg  11597  shftfval  11600  2shfti  11610  caucvgrelemrec  11759  caucvgrelemcau  11760  caucvgre  11761  cvg1nlemcau  11764  cvg1nlemres  11765  resqrexlemcalc3  11796  resqrexlemcvg  11799  resqrexlemglsq  11802  resqrexlemga  11803  sqrtsq  11824  leabs  11854  absexpzap  11861  abslt  11869  absle  11870  abssubap0  11871  caubnd2  11898  icodiamlt  11961  maxleim  11986  maxabslemval  11989  maxleastlt  11996  rexico  12002  zmaxcl  12005  fimaxre2  12008  minmax  12011  zmincl  12020  xrmaxleim  12026  xrmaxiflemcl  12027  xrmaxifle  12028  xrmaxiflemlub  12030  xrmaxiflemval  12032  xrmaxleastlt  12038  xrmaxltsup  12040  xrmaxadd  12043  xrminmax  12047  xrbdtri  12058  climuni  12075  climshftlemg  12084  iserex  12121  climcau  12129  climrecvg1n  12130  climcvg1nlem  12131  sumeq2  12141  summodclem3  12163  zsumdc  12167  isumss  12174  fisumss  12175  sumsnf  12192  fsumconst  12237  modfsummod  12241  fsum00  12245  fsumabs  12248  fsumrelem  12254  fsumiun  12260  isumsplit  12274  divcnv  12280  geo2sum  12297  geoisumr  12301  cvgratz  12315  ntrivcvgap  12331  prodeq2  12340  prodmodclem2  12360  prodmodc  12361  zproddc  12362  fprodmul  12374  prodsnf  12375  fprodcl2lem  12388  fprodconst  12403  fprodap0  12404  fprodrec  12412  fprodap0f  12419  fprodle  12423  fprodmodd  12424  tanaddap  12522  zdvdsdc  12595  dvds2ln  12607  fsumdvds  12625  dvdsle  12627  dvdsext  12638  divalglemeunn  12704  divalglemex  12705  divalglemeuneg  12706  bitsfzo  12738  bitsmod  12739  bitsinv1lem  12744  bitsinv1  12745  dvdsbnd  12749  gcdsupex  12750  gcdsupcl  12751  dvdslegcd  12757  bezoutlemnewy  12789  bezoutlemstep  12790  bezoutlemmain  12791  bezoutlemzz  12795  bezoutlembz  12797  bezoutlembi  12798  bezoutlemle  12801  dfgcd3  12803  bezout  12804  dfgcd2  12807  dvdsmulgcd  12818  bezoutr  12825  uzwodc  12830  nninfctlemfo  12833  lcmval  12857  lcmcllem  12861  lcmneg  12868  ncoprmgcdne1b  12883  isprm2lem  12910  prmind2  12914  dvdsnprmd  12919  isprm5  12937  prmdvdsexp  12943  sqrt2irr  12957  nonsq  13003  sqrtrirr  13005  pceu  13094  pcmul  13100  pc2dvds  13129  pcz  13131  pcprmpw2  13132  dvdsprmpweqle  13136  pcfac  13149  qexpz  13151  prmpwdvds  13154  1arith  13166  mul4sq  13193  4sqexercise2  13198  4sqlemsdc  13199  ballotfilem2  13277  ballotfilemsle  13297  ballotfilemsdom  13304  ballotfilemsima  13308  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ennnfonelemhom  13355  ennnfonelemfun  13357  ennnfonelemf1  13358  ennnfonelemim  13364  exmidunben  13366  ctiunctlemfo  13379  omiunct  13384  ssnnctlemct  13386  isstruct2r  13412  ismgm  13726  issgrp  13767  sgrppropd  13777  sgrpidmndm  13782  mndpropd  13802  issubmnd  13804  resmhm2b  13845  gzsumwmhm  13852  isgrpinv  13908  grplmulf1o  13928  dfgrp3mlem  13952  grplactcnv  13956  mhmid  13967  mhmmnd  13968  ghmgrp  13970  mulgval  13974  mulgfng  13976  mulgnnp1  13982  mulgnn0dir  14004  mulgneg2  14008  mhmmulg  14015  grpissubg  14046  isnsg  14054  isnsg3  14059  nmzsubg  14062  ghmmhmb  14106  ghmpreima  14118  ghmnsgpreima  14121  ghmf1  14125  ghmf1o  14127  conjghm  14128  conjnmz  14131  conjnmzb  14132  ghmcmn  14180  gzsumconst  14192  gsumzfi  14207  gsumclfi  14208  gsummptfidmadd  14210  gsumsubmclfi  14212  gsumconstcmn  14215  prdsval  14222  prdsidlem  14242  pwssub  14265  issrg  14318  srglmhm  14346  srgrmhm  14347  isring  14353  ringadd2  14381  ringlghm  14415  ringrghm  14416  oppr1g  14437  dvdsrvald  14449  dvdsrd  14450  dvdsrex  14454  dvdsrmul1  14458  unitgrp  14472  rhmopp  14532  subrgintm  14600  subrgpropd  14610  isdomn  14627  aprnzr  14648  opprdrng  14669  lmodprop2d  14734  lssvacl  14751  lssvsubcl  14752  lssvscl  14761  lsslss  14767  lss1d  14769  lsspropdg  14817  gsumfsum  14972  expghmap  14991  mulgghm2  14992  znunit  15043  znrrg  15044  issubassa2  15084  assamulgscmlem1  15090  assamulgscmlem2  15091  mplvalcoe  15130  mplsubgfilemcl  15139  mplsubgfileminv  15140  mplsubgfi  15141  opnssneib  15306  restbasg  15318  restopn2  15333  iscnp4  15368  cnss2  15377  cnconst2  15383  cnptopresti  15388  cnptoprest2  15390  neitx  15418  uptx  15424  txrest  15426  txdis1cn  15428  xmetres2  15529  xblss2ps  15554  blhalf  15558  blssps  15577  blss  15578  blssexps  15579  blssex  15580  blin2  15582  metequiv2  15646  bdmetval  15650  metcnp3  15661  metcnp  15662  metcn  15664  metcnpi  15665  metcnpi2  15666  txmetcnp  15668  txmetcn  15669  qtopbas  15672  tgqioo  15705  mpomulcn  15716  fsumcncntop  15717  elcncf2  15724  mulcncflem  15757  mulcncf  15758  suplociccreex  15774  limcdifap  15812  cnplimcim  15817  cnplimccntop  15820  limccnpcntop  15825  dvcj  15859  dvmptfsum  15875  dveflem  15876  ply1termlem  15892  plyaddlem1  15897  plymullem1  15898  plycolemc  15908  plycjlemc  15910  plyrecj  15913  dvply1  15915  reeff1olem  15921  eflt  15925  sin0pilem1  15932  ptolemy  15975  coseq0q4123  15985  coseq0negpitopi  15987  cos02pilt1  16002  cos11  16004  ioocosf1o  16005  logdivlt  16046  logdivle  16047  rpcxpmul2  16068  cxplt  16071  cxple  16072  cxplt3  16075  apcxp2  16094  rprelogbmul  16110  rprelogbdiv  16112  birthdaylem3  16146  pellexlem3  16150  ppiqltx  16183  dvdsppwf1o  16184  perfect  16199  bcmax  16203  bposlem3  16211  lgsval  16221  lgsfcl2  16223  lgscllem  16224  lgsval2lem  16227  lgsdir2lem4  16248  lgsdir2lem5  16249  lgsdir2  16250  lgsne0  16255  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  2sqlem6  16337  2sqlem10  16342  umgrnloopv  16453  umgrvad2edg  16550  usgr1eop  16584  wlkvtxiedg  16684  wlkvtxiedgg  16685  upgredginwlk  16695  upgriswlkdc  16699  clwwlkccatlem  16739  eupth2lem3lem4fi  16812  pw1ndom3  17118  pw1map  17123  pwle2  17126  pwf1oexmid  17127  subctctexmid  17128  pw1nct  17131  stnot  17137  peano4nninf  17147  nninfalllem1  17149  nninfall  17150  nninfsellemeq  17155  nninfsellemqall  17156  nnnninfex  17163  nninfnfiinf  17164  sbthom  17169  refeq  17171  isomninnlem  17177  trilpolemeq1  17187  trilpolemlt1  17188  trirec0  17191  apdiff  17195  iswomninnlem  17197  ismkvnnlem  17200  redcwlpolemeq1  17202  ltlenmkv  17218