Theorem simplr 520

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 481	1 |- ( ( ( ph /\ ps ) /\ ch ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp1lr  1051  simp2lr  1055  simp3lr  1059  bilukdc  1386  dcun  3519  intab  3853  exmid01  4177  exmidundif  4185  exmidundifim  4186  frirrg  4328  reg2exmidlema  4511  imadiflem  5267  fvco4  5558  fvmptt  5577  fcoconst  5656  f1imass  5742  fcof1  5751  fliftfun  5764  riotass2  5824  ovmpodxf  5967  dftpos4  6231  tfrlem1  6276  tfrlem3ag  6277  tfrlemibacc  6294  tfrlemibfn  6296  tfrlemi1  6300  tfrlemi14d  6301  tfr1onlem3ag  6305  tfr1onlembacc  6310  tfr1onlembfn  6312  tfr1onlemaccex  6316  tfrcllembacc  6323  tfrcllembfn  6325  tfrcllemaccex  6329  frecabcl  6367  nntr2  6471  dcdifsnid  6472  nnm00  6497  ecopovsymg  6600  ecopoverg  6602  th3qlem1  6603  mapss  6657  f1imaen2g  6759  xpen  6811  xpmapenlem  6815  phpm  6831  fidifsnen  6836  dif1enen  6846  fiunsnnn  6847  fin0  6851  fin0or  6852  findcard2d  6857  findcard2sd  6858  diffifi  6860  isinfinf  6863  tridc  6865  fimax2gtrilemstep  6866  fimax2gtri  6867  en2eqpr  6873  onunsnss  6882  unsnfidcex  6885  unsnfidcel  6886  undifdcss  6888  unfiin  6891  fisseneq  6897  ssfirab  6899  f1finf1o  6912  fidcenumlemrks  6918  fidcenumlemrk  6919  fidcenumlemr  6920  fidcenum  6921  suplub2ti  6966  supisolem  6973  ordiso2  7000  djudom  7058  omp1eomlem  7059  difinfsnlem  7064  difinfinf  7066  ctm  7074  ctssdclemn0  7075  enumct  7080  nnnninfeq  7092  nnnninfeq2  7093  nninfisol  7097  enomnilem  7102  finomni  7104  exmidomni  7106  fodju0  7111  ismkvnex  7119  enmkvlem  7125  enwomnilem  7133  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  exmidaclem  7164  exmidontriimlem1  7177  exmidontriimlem2  7178  exmidontriimlem3  7179  exmidontriimlem4  7180  exmidontriim  7181  dfplpq2  7295  dfmpq2  7296  mulpipqqs  7314  nqpi  7319  distrnqg  7328  prarloclemarch  7359  enq0tr  7375  nqnq0pi  7379  nq0nn  7383  nnnq0lem1  7387  prarloclemup  7436  prarloclem3  7438  prarloclemcalc  7443  genplt2i  7451  addnqprllem  7468  addnqprulem  7469  appdivnq  7504  distrlem1prl  7523  distrlem1pru  7524  ltaddpr  7538  ltexprlemlol  7543  ltexprlemupu  7545  ltexprlemdisj  7547  addcanprleml  7555  ltaprlem  7559  addextpr  7562  recexprlemopu  7568  recexprlemdisj  7571  recexprlem1ssl  7574  aptiprleml  7580  cauappcvgprlemm  7586  cauappcvgprlemopl  7587  cauappcvgprlemlol  7588  cauappcvgprlemopu  7589  cauappcvgprlemdisj  7592  cauappcvgprlemladdfu  7595  cauappcvgprlemladdfl  7596  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  caucvgprlemm  7609  caucvgprlemopl  7610  caucvgprlemlol  7611  caucvgprlemopu  7612  caucvgprlemladdfu  7618  caucvgprprlemml  7635  caucvgprprlemopl  7638  caucvgprprlemlol  7639  caucvgprprlemopu  7640  caucvgprprlemexbt  7647  suplocexprlemru  7660  suplocexprlemloc  7662  suplocexprlemub  7664  suplocexprlemlub  7665  prsrlem1  7683  recexgt0sr  7714  mulgt0sr  7719  archsr  7723  caucvgsrlemcau  7734  caucvgsrlemoffcau  7739  caucvgsrlemoffres  7741  suplocsrlemb  7747  suplocsrlempr  7748  suplocsrlem  7749  addcnsr  7775  mulcnsr  7776  mulcnsrec  7784  axmulcom  7812  nntopi  7835  axcaucvglemcau  7839  axcaucvglemres  7840  axpre-suploclemres  7842  axpre-suploc  7843  axsuploc  7971  ltntri  8026  cnegexlem2  8074  cnegexlem3  8075  addsub4  8141  le2add  8342  lt2add  8343  lt2sub  8358  le2sub  8359  rereim  8484  apreim  8501  mulreim  8502  apcotr  8505  apadd1  8506  addext  8508  mulext1  8510  mulext  8512  apti  8520  receuap  8566  rec11rap  8607  divdivdivap  8609  divadddivap  8623  divsubdivap  8624  rerecclap  8626  recgt0  8745  prodgt0gt0  8746  prodgt0  8747  prodge0  8749  lemulge11  8761  lt2mul2div  8774  ltrec  8778  lerec  8779  ltrec1  8783  lediv2a  8790  mulle0r  8839  sup3exmid  8852  zdiv  9279  eluzuzle  9474  supinfneg  9533  infsupneg  9534  infregelbex  9536  xrltso  9732  xnn0dcle  9738  xnn0letri  9739  npnflt  9751  nmnfgt  9754  z2ge  9762  xaddf  9780  xaddval  9781  xpncan  9807  xleadd1a  9809  xltadd1  9812  xaddge0  9814  xle2add  9815  xleaddadd  9823  ixxss1  9840  ixxss2  9841  elico2  9873  iccsupr  9902  fzass4  9997  fzrev  10019  fz0fzelfz0  10062  fzocatel  10134  elfzomelpfzo  10166  exbtwnzlemstep  10183  rebtwn2zlemstep  10188  qbtwnxr  10193  apbtwnz  10209  btwnzge0  10235  modqid  10284  modqcyc  10294  modqcyc2  10295  modqaddabs  10297  modqaddmod  10298  mulqaddmodid  10299  modqmuladd  10301  modqltm1p1mod  10311  modqsubmod  10317  modqsubmodmod  10318  modaddmodlo  10323  modqmulmod  10324  modqmulmodr  10325  modqsubdir  10328  addmodlteq  10333  iseqf1olemab  10424  iseqf1olemmo  10427  iseqf1olemjpcl  10430  iseqf1olemqpcl  10431  exp3val  10457  expcl2lemap  10467  expap0  10485  expnegzap  10489  expmul  10500  leexp1a  10510  qsqeqor  10565  expnbnd  10578  nn0ltexp2  10623  nn0opth2  10637  facndiv  10652  faclbnd  10654  bcval5  10676  bcpasc  10679  hashennnuni  10692  hashunlem  10717  hashunsng  10720  hashprg  10721  fiprsshashgt1  10730  hashxp  10739  fimaxq  10740  zfz1isolemiso  10752  zfz1isolem1  10753  seq3coll  10755  shftlem  10758  shftfvalg  10760  shftfval  10763  2shfti  10773  caucvgrelemrec  10921  caucvgrelemcau  10922  caucvgre  10923  cvg1nlemcau  10926  cvg1nlemres  10927  resqrexlemcalc3  10958  resqrexlemcvg  10961  resqrexlemglsq  10964  resqrexlemga  10965  sqrtsq  10986  leabs  11016  absexpzap  11022  abslt  11030  absle  11031  abssubap0  11032  caubnd2  11059  icodiamlt  11122  maxleim  11147  maxabslemval  11150  maxleastlt  11157  rexico  11163  zmaxcl  11166  fimaxre2  11168  minmax  11171  xrmaxleim  11185  xrmaxiflemcl  11186  xrmaxifle  11187  xrmaxiflemlub  11189  xrmaxiflemval  11191  xrmaxleastlt  11197  xrmaxltsup  11199  xrmaxadd  11202  xrminmax  11206  xrbdtri  11217  climuni  11234  climshftlemg  11243  iserex  11280  climcau  11288  climrecvg1n  11289  climcvg1nlem  11290  sumeq2  11300  summodclem3  11321  zsumdc  11325  isumss  11332  fisumss  11333  sumsnf  11350  fsumconst  11395  modfsummod  11399  fsum00  11403  fsumabs  11406  fsumrelem  11412  fsumiun  11418  isumsplit  11432  divcnv  11438  geo2sum  11455  geoisumr  11459  cvgratz  11473  ntrivcvgap  11489  prodeq2  11498  prodmodclem2  11518  prodmodc  11519  zproddc  11520  fprodmul  11532  prodsnf  11533  fprodcl2lem  11546  fprodconst  11561  fprodap0  11562  fprodrec  11570  fprodap0f  11577  fprodle  11581  fprodmodd  11582  tanaddap  11680  zdvdsdc  11752  dvds2ln  11764  dvdsle  11782  dvdsext  11793  divalglemeunn  11858  divalglemex  11859  divalglemeuneg  11860  zsupcllemstep  11878  dvdsbnd  11889  gcdsupex  11890  gcdsupcl  11891  dvdslegcd  11897  bezoutlemnewy  11929  bezoutlemstep  11930  bezoutlemmain  11931  bezoutlemzz  11935  bezoutlembz  11937  bezoutlembi  11938  bezoutlemle  11941  dfgcd3  11943  bezout  11944  dfgcd2  11947  dvdsmulgcd  11958  bezoutr  11965  uzwodc  11970  lcmval  11995  lcmcllem  11999  lcmneg  12006  ncoprmgcdne1b  12021  isprm2lem  12048  prmind2  12052  dvdsnprmd  12057  isprm5  12074  prmdvdsexp  12080  sqrt2irr  12094  oddpwdclemxy  12101  oddpwdclemdc  12105  nonsq  12139  pceu  12227  pcmul  12233  pc2dvds  12261  pcz  12263  pcprmpw2  12264  dvdsprmpweqle  12268  pcfac  12280  qexpz  12282  prmpwdvds  12285  1arith  12297  mul4sq  12324  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ennnfonelemhom  12348  ennnfonelemfun  12350  ennnfonelemf1  12351  ennnfonelemim  12357  exmidunben  12359  ctiunctlemfo  12372  omiunct  12377  ssnnctlemct  12379  isstruct2r  12405  ismgm  12588  issgrp  12621  opnssneib  12806  restbasg  12818  restopn2  12833  iscnp4  12868  cnss2  12877  cnconst2  12883  cnptopresti  12888  cnptoprest2  12890  neitx  12918  uptx  12924  txrest  12926  txdis1cn  12928  xmetres2  13029  xblss2ps  13054  blhalf  13058  blssps  13077  blss  13078  blssexps  13079  blssex  13080  blin2  13082  metequiv2  13146  bdmetval  13150  metcnp3  13161  metcnp  13162  metcn  13164  metcnpi  13165  metcnpi2  13166  txmetcnp  13168  txmetcn  13169  qtopbas  13172  tgqioo  13197  fsumcncntop  13206  elcncf2  13211  mulcncflem  13240  mulcncf  13241  suplociccreex  13252  limcdifap  13281  cnplimcim  13286  cnplimccntop  13289  limccnpcntop  13294  dvcj  13323  dveflem  13337  reeff1olem  13342  eflt  13346  sin0pilem1  13352  ptolemy  13395  coseq0q4123  13405  coseq0negpitopi  13407  cos02pilt1  13422  cos11  13424  ioocosf1o  13425  cxplt  13486  cxple  13487  cxplt3  13490  apcxp2  13508  rprelogbmul  13523  rprelogbdiv  13525  lgsval  13555  lgsfcl2  13557  lgscllem  13558  lgsval2lem  13561  lgsdir2lem4  13582  lgsdir2lem5  13583  lgsdir2  13584  lgsne0  13589  2sqlem6  13606  2sqlem10  13611  pwle2  13888  pwf1oexmid  13889  subctctexmid  13891  pw1nct  13893  peano4nninf  13896  nninfalllem1  13898  nninfall  13899  nninfsellemeq  13904  nninfsellemqall  13905  sbthom  13915  refeq  13917  isomninnlem  13919  trilpolemeq1  13929  trilpolemlt1  13930  trirec0  13933  apdiff  13937  iswomninnlem  13938  ismkvnnlem  13941  redcwlpolemeq1  13943