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 )

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  1092  simp2lr  1096  simp3lr  1100  bilukdc  1445  dcun  3634  ifnefals  3682  ifeqeqxdc  3684  intab  3994  exmid01  4330  exmidundif  4338  exmidundifim  4339  frirrg  4490  reg2exmidlema  4676  imadiflem  5455  fvco4  5771  fvmptt  5791  fcoconst  5870  funopsn  5882  f1imass  5970  fcof1  5979  fliftfun  5992  riotass2  6057  ovmpodxf  6204  fsuppeq  6477  fsuppeqg  6478  suppssdc  6490  suppssfvg  6493  dftpos4  6524  tfrlem1  6569  tfrlem3ag  6570  tfrlemibacc  6587  tfrlemibfn  6589  tfrlemi1  6593  tfrlemi14d  6594  tfr1onlem3ag  6598  tfr1onlembacc  6603  tfr1onlembfn  6605  tfr1onlemaccex  6609  tfrcllembacc  6616  tfrcllembfn  6618  tfrcllemaccex  6622  frecabcl  6660  nntr2  6766  dcdifsnid  6767  nnm00  6793  ecopovsymg  6898  ecopoverg  6900  th3qlem1  6901  mapss  6963  f1imaen2g  7070  pw2f1odclem  7124  xpen  7135  xpmapenlem  7139  mapunen  7141  phpm  7157  fidifsnen  7162  dif1enen  7174  fiunsnnn  7175  fin0  7179  fin0or  7180  findcard2d  7185  findcard2sd  7186  diffifi  7188  isinfinf  7191  tridc  7194  fimax2gtrilemstep  7195  fimax2gtri  7196  en2eqpr  7204  onunsnss  7214  unsnfidcex  7217  unsnfidcel  7218  undifdcss  7220  unfiin  7223  fisseneq  7232  ssfirab  7234  f1finf1o  7254  fidcenumlemrks  7260  fidcenumlemrk  7261  fidcenumlemr  7262  fidcenum  7263  ffsuppbi  7290  fdcf1  7306  f1setfi  7307  2omap  7308  suplub2ti  7331  supisolem  7338  ordiso2  7365  djudom  7423  omp1eomlem  7424  difinfsnlem  7429  difinfinf  7431  ctm  7439  ctssdclemn0  7440  enumct  7445  nnnninfeq  7458  nnnninfeq2  7459  nninfisol  7463  enomnilem  7468  finomni  7470  exmidomni  7472  fodju0  7477  ismkvnex  7485  enmkvlem  7491  enwomnilem  7499  pr2cv1  7531  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  exmidaclem  7554  exmidontriimlem1  7567  exmidontriimlem2  7568  exmidontriimlem3  7569  exmidontriimlem4  7570  exmidontriim  7571  netap  7610  exmidapne  7616  dfplpq2  7711  dfmpq2  7712  mulpipqqs  7730  nqpi  7735  distrnqg  7744  prarloclemarch  7775  enq0tr  7791  nqnq0pi  7795  nq0nn  7799  nnnq0lem1  7803  prarloclemup  7852  prarloclem3  7854  prarloclemcalc  7859  genplt2i  7867  addnqprllem  7884  addnqprulem  7885  appdivnq  7920  distrlem1prl  7939  distrlem1pru  7940  ltaddpr  7954  ltexprlemlol  7959  ltexprlemupu  7961  ltexprlemdisj  7963  addcanprleml  7971  ltaprlem  7975  addextpr  7978  recexprlemopu  7984  recexprlemdisj  7987  recexprlem1ssl  7990  aptiprleml  7996  cauappcvgprlemm  8002  cauappcvgprlemopl  8003  cauappcvgprlemlol  8004  cauappcvgprlemopu  8005  cauappcvgprlemdisj  8008  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemlol  8027  caucvgprlemopu  8028  caucvgprlemladdfu  8034  caucvgprprlemml  8051  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemopu  8056  caucvgprprlemexbt  8063  suplocexprlemru  8076  suplocexprlemloc  8078  suplocexprlemub  8080  suplocexprlemlub  8081  prsrlem1  8099  recexgt0sr  8130  mulgt0sr  8135  archsr  8139  caucvgsrlemcau  8150  caucvgsrlemoffcau  8155  caucvgsrlemoffres  8157  suplocsrlemb  8163  suplocsrlempr  8164  suplocsrlem  8165  addcnsr  8191  mulcnsr  8192  mulcnsrec  8200  axmulcom  8228  nntopi  8251  axcaucvglemcau  8255  axcaucvglemres  8256  axpre-suploclemres  8258  axpre-suploc  8259  mpomulf  8306  axsuploc  8388  ltntri  8444  cnegexlem2  8492  cnegexlem3  8493  addsub4  8559  le2add  8762  lt2add  8763  lt2sub  8778  le2sub  8779  rereim  8904  apreim  8921  mulreim  8922  apcotr  8925  apadd1  8926  addext  8928  mulext1  8930  mulext  8932  apti  8940  aptap  8968  receuap  8989  rec11rap  9031  divdivdivap  9033  divadddivap  9047  divsubdivap  9048  rerecclap  9050  recgt0  9170  prodgt0gt0  9171  prodgt0  9172  prodge0  9174  lemulge11  9186  lt2mul2div  9199  ltrec  9203  lerec  9204  ltrec1  9208  lediv2a  9215  mulle0r  9264  sup3exmid  9277  zdiv  9713  eluzuzle  9909  supinfneg  9974  infsupneg  9975  infregelbex  9977  xrltso  10177  xnn0dcle  10183  xnn0letri  10184  npnflt  10196  nmnfgt  10199  z2ge  10207  xaddf  10225  xaddval  10226  xpncan  10252  xleadd1a  10254  xltadd1  10257  xaddge0  10259  xle2add  10260  xleaddadd  10268  ixxss1  10285  ixxss2  10286  elico2  10318  iccsupr  10347  fzass4  10446  fzrev  10469  fz0fzelfz0  10512  fzocatel  10595  elfzomelpfzo  10627  zsupcllemstep  10640  exbtwnzlemstep  10660  rebtwn2zlemstep  10665  qbtwnxr  10670  xqltnle  10680  apbtwnz  10687  btwnzge0  10713  modqid  10764  modqcyc  10774  modqcyc2  10775  modqaddabs  10777  modqaddmod  10778  mulqaddmodid  10779  modqmuladd  10781  modqltm1p1mod  10791  modqsubmod  10797  modqsubmodmod  10798  modaddmodlo  10803  modqmulmod  10804  modqmulmodr  10805  modqsubdir  10808  addmodlteq  10813  nninfinf  10858  iseqf1olemab  10917  iseqf1olemmo  10920  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  seqf1oglem1  10934  seqf1oglem2  10935  seqf1og  10936  exp3val  10956  expcl2lemap  10966  expap0  10984  expnegzap  10988  expmul  10999  leexp1a  11009  qsqeqor  11065  resq01  11073  expnbnd  11079  nn0ltexp2  11125  nn0opth2  11140  facndiv  11155  faclbnd  11157  bcval5  11179  bcpasc  11182  hashennnuni  11196  hashunlem  11222  hashunsng  11226  hashprg  11227  fiprsshashgt1  11236  hashxp  11245  fimaxq  11248  hashfibc  11261  zfz1isolemiso  11269  zfz1isolem1  11270  seq3coll  11272  iswrdiz  11289  wrdnval  11313  ccatlen  11341  ccatvalfn  11347  ccatsymb  11348  ccatalpha  11359  ccat2s1fstg  11394  swrdclg  11400  swrdsb0eq  11415  pfxwrdsymbg  11440  wrdind  11472  wrd2ind  11473  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12  11483  pfxccat3  11484  swrdccat  11485  shftlem  11559  shftfvalg  11561  shftfval  11564  2shfti  11574  caucvgrelemrec  11723  caucvgrelemcau  11724  caucvgre  11725  cvg1nlemcau  11728  cvg1nlemres  11729  resqrexlemcalc3  11760  resqrexlemcvg  11763  resqrexlemglsq  11766  resqrexlemga  11767  sqrtsq  11788  leabs  11818  absexpzap  11824  abslt  11832  absle  11833  abssubap0  11834  caubnd2  11861  icodiamlt  11924  maxleim  11949  maxabslemval  11952  maxleastlt  11959  rexico  11965  zmaxcl  11968  fimaxre2  11971  minmax  11974  xrmaxleim  11988  xrmaxiflemcl  11989  xrmaxifle  11990  xrmaxiflemlub  11992  xrmaxiflemval  11994  xrmaxleastlt  12000  xrmaxltsup  12002  xrmaxadd  12005  xrminmax  12009  xrbdtri  12020  climuni  12037  climshftlemg  12046  iserex  12083  climcau  12091  climrecvg1n  12092  climcvg1nlem  12093  sumeq2  12103  summodclem3  12125  zsumdc  12129  isumss  12136  fisumss  12137  sumsnf  12154  fsumconst  12199  modfsummod  12203  fsum00  12207  fsumabs  12210  fsumrelem  12216  fsumiun  12222  isumsplit  12236  divcnv  12242  geo2sum  12259  geoisumr  12263  cvgratz  12277  ntrivcvgap  12293  prodeq2  12302  prodmodclem2  12322  prodmodc  12323  zproddc  12324  fprodmul  12336  prodsnf  12337  fprodcl2lem  12350  fprodconst  12365  fprodap0  12366  fprodrec  12374  fprodap0f  12381  fprodle  12385  fprodmodd  12386  tanaddap  12484  zdvdsdc  12557  dvds2ln  12569  fsumdvds  12587  dvdsle  12589  dvdsext  12600  divalglemeunn  12666  divalglemex  12667  divalglemeuneg  12668  bitsfzo  12700  bitsmod  12701  bitsinv1lem  12706  bitsinv1  12707  dvdsbnd  12711  gcdsupex  12712  gcdsupcl  12713  dvdslegcd  12719  bezoutlemnewy  12751  bezoutlemstep  12752  bezoutlemmain  12753  bezoutlemzz  12757  bezoutlembz  12759  bezoutlembi  12760  bezoutlemle  12763  dfgcd3  12765  bezout  12766  dfgcd2  12769  dvdsmulgcd  12780  bezoutr  12787  uzwodc  12792  nninfctlemfo  12795  lcmval  12819  lcmcllem  12823  lcmneg  12830  ncoprmgcdne1b  12845  isprm2lem  12872  prmind2  12876  dvdsnprmd  12881  isprm5  12898  prmdvdsexp  12904  sqrt2irr  12918  oddpwdclemxy  12925  oddpwdclemdc  12929  nonsq  12963  pceu  13052  pcmul  13058  pc2dvds  13087  pcz  13089  pcprmpw2  13090  dvdsprmpweqle  13094  pcfac  13107  qexpz  13109  prmpwdvds  13112  1arith  13124  mul4sq  13151  4sqexercise2  13156  4sqlemsdc  13157  ballotfilem2  13206  ballotfilemsle  13226  ballotfilemsdom  13233  ballotfilemsima  13237  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemhom  13284  ennnfonelemfun  13286  ennnfonelemf1  13287  ennnfonelemim  13293  exmidunben  13295  ctiunctlemfo  13308  omiunct  13313  ssnnctlemct  13315  isstruct2r  13341  ismgm  13654  issgrp  13695  sgrppropd  13705  sgrpidmndm  13710  mndpropd  13730  issubmnd  13732  resmhm2b  13773  gzsumwmhm  13780  isgrpinv  13836  grplmulf1o  13856  dfgrp3mlem  13880  grplactcnv  13884  mhmid  13895  mhmmnd  13896  ghmgrp  13898  mulgval  13902  mulgfng  13904  mulgnnp1  13910  mulgnn0dir  13932  mulgneg2  13936  mhmmulg  13943  grpissubg  13974  isnsg  13982  isnsg3  13987  nmzsubg  13990  ghmmhmb  14034  ghmpreima  14046  ghmnsgpreima  14049  ghmf1  14053  ghmf1o  14055  conjghm  14056  conjnmz  14059  conjnmzb  14060  ghmcmn  14108  gzsumconst  14120  gsumzfi  14135  gsumclfi  14136  gsummptfidmadd  14138  gsumsubmclfi  14140  gsumconstcmn  14143  prdsval  14150  prdsidlem  14170  pwssub  14193  issrg  14243  srglmhm  14271  srgrmhm  14272  isring  14278  ringadd2  14305  ringlghm  14339  ringrghm  14340  oppr1g  14361  dvdsrvald  14373  dvdsrd  14374  dvdsrex  14378  dvdsrmul1  14382  unitgrp  14396  rhmopp  14456  subrgintm  14524  subrgpropd  14534  isdomn  14551  aprnzr  14572  opprdrng  14593  lmodprop2d  14657  lssvacl  14674  lssvsubcl  14675  lssvscl  14684  lsslss  14690  lss1d  14692  lsspropdg  14740  gsumfsum  14895  expghmap  14914  mulgghm2  14915  znunit  14966  znrrg  14967  mplvalcoe  15004  mplsubgfilemcl  15013  mplsubgfileminv  15014  mplsubgfi  15015  opnssneib  15180  restbasg  15192  restopn2  15207  iscnp4  15242  cnss2  15251  cnconst2  15257  cnptopresti  15262  cnptoprest2  15264  neitx  15292  uptx  15298  txrest  15300  txdis1cn  15302  xmetres2  15403  xblss2ps  15428  blhalf  15432  blssps  15451  blss  15452  blssexps  15453  blssex  15454  blin2  15456  metequiv2  15520  bdmetval  15524  metcnp3  15535  metcnp  15536  metcn  15538  metcnpi  15539  metcnpi2  15540  txmetcnp  15542  txmetcn  15543  qtopbas  15546  tgqioo  15579  mpomulcn  15590  fsumcncntop  15591  elcncf2  15598  mulcncflem  15631  mulcncf  15632  suplociccreex  15648  limcdifap  15686  cnplimcim  15691  cnplimccntop  15694  limccnpcntop  15699  dvcj  15733  dvmptfsum  15749  dveflem  15750  ply1termlem  15766  plyaddlem1  15771  plymullem1  15772  plycolemc  15782  plycjlemc  15784  plyrecj  15787  dvply1  15789  reeff1olem  15795  eflt  15799  sin0pilem1  15805  ptolemy  15848  coseq0q4123  15858  coseq0negpitopi  15860  cos02pilt1  15875  cos11  15877  ioocosf1o  15878  rpcxpmul2  15938  cxplt  15941  cxple  15942  cxplt3  15945  apcxp2  15964  rprelogbmul  15980  rprelogbdiv  15982  pellexlem3  16007  dvdsppwf1o  16017  perfect  16029  lgsval  16037  lgsfcl2  16039  lgscllem  16040  lgsval2lem  16043  lgsdir2lem4  16064  lgsdir2lem5  16065  lgsdir2  16066  lgsne0  16071  gausslemma2dlem1a  16091  gausslemma2dlem1f1o  16093  2sqlem6  16153  2sqlem10  16158  umgrnloopv  16269  umgrvad2edg  16366  usgr1eop  16400  wlkvtxiedg  16500  wlkvtxiedgg  16501  upgredginwlk  16511  upgriswlkdc  16515  clwwlkccatlem  16555  eupth2lem3lem4fi  16628  pw1ndom3  16934  pw1map  16939  pwle2  16942  pwf1oexmid  16943  subctctexmid  16944  pw1nct  16947  peano4nninf  16954  nninfalllem1  16956  nninfall  16957  nninfsellemeq  16962  nninfsellemqall  16963  nnnninfex  16970  nninfnfiinf  16971  sbthom  16976  refeq  16978  isomninnlem  16984  trilpolemeq1  16994  trilpolemlt1  16995  trirec0  16998  apdiff  17002  iswomninnlem  17004  ismkvnnlem  17007  redcwlpolemeq1  17009  ltlenmkv  17025