Theorem simplr 519

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 480	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  1045  simp2lr  1049  simp3lr  1053  bilukdc  1374  dcun  3468  intab  3795  exmid01  4116  exmidundif  4124  exmidundifim  4125  frirrg  4267  reg2exmidlema  4444  imadiflem  5197  fvco4  5486  fvmptt  5505  fcoconst  5584  f1imass  5668  fcof1  5677  fliftfun  5690  riotass2  5749  ovmpodxf  5889  dftpos4  6153  tfrlem1  6198  tfrlem3ag  6199  tfrlemibacc  6216  tfrlemibfn  6218  tfrlemi1  6222  tfrlemi14d  6223  tfr1onlem3ag  6227  tfr1onlembacc  6232  tfr1onlembfn  6234  tfr1onlemaccex  6238  tfrcllembacc  6245  tfrcllembfn  6247  tfrcllemaccex  6251  frecabcl  6289  nntr2  6392  dcdifsnid  6393  nnm00  6418  ecopovsymg  6521  ecopoverg  6523  th3qlem1  6524  mapss  6578  f1imaen2g  6680  xpen  6732  xpmapenlem  6736  phpm  6752  fidifsnen  6757  dif1enen  6767  fiunsnnn  6768  fin0  6772  fin0or  6773  findcard2d  6778  findcard2sd  6779  diffifi  6781  isinfinf  6784  tridc  6786  fimax2gtrilemstep  6787  fimax2gtri  6788  en2eqpr  6794  onunsnss  6798  unsnfidcex  6801  unsnfidcel  6802  undifdcss  6804  unfiin  6807  fisseneq  6813  ssfirab  6815  f1finf1o  6828  fidcenumlemrks  6834  fidcenumlemrk  6835  fidcenumlemr  6836  fidcenum  6837  suplub2ti  6881  supisolem  6888  ordiso2  6913  djudom  6971  omp1eomlem  6972  difinfsnlem  6977  difinfinf  6979  ctm  6987  ctssdclemn0  6988  enumct  6993  enomnilem  7003  finomni  7005  exmidomni  7007  fodju0  7012  ismkvnex  7022  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  exmidaclem  7057  dfplpq2  7155  dfmpq2  7156  mulpipqqs  7174  nqpi  7179  distrnqg  7188  prarloclemarch  7219  enq0tr  7235  nqnq0pi  7239  nq0nn  7243  nnnq0lem1  7247  prarloclemup  7296  prarloclem3  7298  prarloclemcalc  7303  genplt2i  7311  addnqprllem  7328  addnqprulem  7329  appdivnq  7364  distrlem1prl  7383  distrlem1pru  7384  ltaddpr  7398  ltexprlemlol  7403  ltexprlemupu  7405  ltexprlemdisj  7407  addcanprleml  7415  ltaprlem  7419  addextpr  7422  recexprlemopu  7428  recexprlemdisj  7431  recexprlem1ssl  7434  aptiprleml  7440  cauappcvgprlemm  7446  cauappcvgprlemopl  7447  cauappcvgprlemlol  7448  cauappcvgprlemopu  7449  cauappcvgprlemdisj  7452  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  caucvgprlemm  7469  caucvgprlemopl  7470  caucvgprlemlol  7471  caucvgprlemopu  7472  caucvgprlemladdfu  7478  caucvgprprlemml  7495  caucvgprprlemopl  7498  caucvgprprlemlol  7499  caucvgprprlemopu  7500  caucvgprprlemexbt  7507  suplocexprlemru  7520  suplocexprlemloc  7522  suplocexprlemub  7524  suplocexprlemlub  7525  prsrlem1  7543  recexgt0sr  7574  mulgt0sr  7579  archsr  7583  caucvgsrlemcau  7594  caucvgsrlemoffcau  7599  caucvgsrlemoffres  7601  suplocsrlemb  7607  suplocsrlempr  7608  suplocsrlem  7609  addcnsr  7635  mulcnsr  7636  mulcnsrec  7644  axmulcom  7672  nntopi  7695  axcaucvglemcau  7699  axcaucvglemres  7700  axpre-suploclemres  7702  axpre-suploc  7703  axsuploc  7830  ltntri  7883  cnegexlem2  7931  cnegexlem3  7932  addsub4  7998  le2add  8199  lt2add  8200  lt2sub  8215  le2sub  8216  rereim  8341  apreim  8358  mulreim  8359  apcotr  8362  apadd1  8363  addext  8365  mulext1  8367  mulext  8369  apti  8377  receuap  8423  rec11rap  8464  divdivdivap  8466  divadddivap  8480  divsubdivap  8481  rerecclap  8483  recgt0  8601  prodgt0gt0  8602  prodgt0  8603  prodge0  8605  lemulge11  8617  lt2mul2div  8630  ltrec  8634  lerec  8635  ltrec1  8639  lediv2a  8646  mulle0r  8695  sup3exmid  8708  zdiv  9132  eluzuzle  9327  supinfneg  9383  infsupneg  9384  xrltso  9575  npnflt  9591  nmnfgt  9594  z2ge  9602  xaddf  9620  xaddval  9621  xpncan  9647  xleadd1a  9649  xltadd1  9652  xaddge0  9654  xle2add  9655  xleaddadd  9663  ixxss1  9680  ixxss2  9681  elico2  9713  iccsupr  9742  fzass4  9835  fzrev  9857  fz0fzelfz0  9897  fzocatel  9969  elfzomelpfzo  10001  exbtwnzlemstep  10018  rebtwn2zlemstep  10023  qbtwnxr  10028  apbtwnz  10040  btwnzge0  10066  modqid  10115  modqcyc  10125  modqcyc2  10126  modqaddabs  10128  modqaddmod  10129  mulqaddmodid  10130  modqmuladd  10132  modqltm1p1mod  10142  modqsubmod  10148  modqsubmodmod  10149  modaddmodlo  10154  modqmulmod  10155  modqmulmodr  10156  modqsubdir  10159  addmodlteq  10164  iseqf1olemab  10255  iseqf1olemmo  10258  iseqf1olemjpcl  10261  iseqf1olemqpcl  10262  exp3val  10288  expcl2lemap  10298  expap0  10316  expnegzap  10320  expmul  10331  leexp1a  10341  expnbnd  10408  nn0opth2  10463  facndiv  10478  faclbnd  10480  bcval5  10502  bcpasc  10505  hashennnuni  10518  hashunlem  10543  hashunsng  10546  hashprg  10547  fiprsshashgt1  10556  hashxp  10565  fimaxq  10566  zfz1isolemiso  10575  zfz1isolem1  10576  seq3coll  10578  shftlem  10581  shftfvalg  10583  shftfval  10586  2shfti  10596  caucvgrelemrec  10744  caucvgrelemcau  10745  caucvgre  10746  cvg1nlemcau  10749  cvg1nlemres  10750  resqrexlemcalc3  10781  resqrexlemcvg  10784  resqrexlemglsq  10787  resqrexlemga  10788  sqrtsq  10809  leabs  10839  absexpzap  10845  abslt  10853  absle  10854  abssubap0  10855  caubnd2  10882  icodiamlt  10945  maxleim  10970  maxabslemval  10973  maxleastlt  10980  rexico  10986  zmaxcl  10989  fimaxre2  10991  minmax  10994  xrmaxleim  11006  xrmaxiflemcl  11007  xrmaxifle  11008  xrmaxiflemlub  11010  xrmaxiflemval  11012  xrmaxleastlt  11018  xrmaxltsup  11020  xrmaxadd  11023  xrminmax  11027  xrbdtri  11038  climuni  11055  climshftlemg  11064  iserex  11101  climcau  11109  climrecvg1n  11110  climcvg1nlem  11111  sumeq2  11121  summodclem3  11142  zsumdc  11146  isumss  11153  fisumss  11154  sumsnf  11171  fsumconst  11216  modfsummod  11220  fsum00  11224  fsumabs  11227  fsumrelem  11233  fsumiun  11239  isumsplit  11253  divcnv  11259  geo2sum  11276  geoisumr  11280  cvgratz  11294  ntrivcvgap  11310  prodeq2  11319  tanaddap  11435  zdvdsdc  11503  dvds2ln  11515  dvdsle  11531  dvdsext  11542  divalglemeunn  11607  divalglemex  11608  divalglemeuneg  11609  zsupcllemstep  11627  dvdsbnd  11634  gcdsupex  11635  gcdsupcl  11636  dvdslegcd  11642  bezoutlemnewy  11673  bezoutlemstep  11674  bezoutlemmain  11675  bezoutlemzz  11679  bezoutlembz  11681  bezoutlembi  11682  bezoutlemle  11685  dfgcd3  11687  bezout  11688  dfgcd2  11691  dvdsmulgcd  11702  bezoutr  11709  lcmval  11733  lcmcllem  11737  lcmneg  11744  ncoprmgcdne1b  11759  isprm2lem  11786  prmind2  11790  dvdsnprmd  11795  prmdvdsexp  11815  sqrt2irr  11829  oddpwdclemxy  11836  oddpwdclemdc  11840  nonsq  11874  ennnfonelemkh  11914  ennnfonelemhf1o  11915  ennnfonelemhom  11917  ennnfonelemfun  11919  ennnfonelemf1  11920  ennnfonelemim  11926  exmidunben  11928  ctiunctlemfo  11941  isstruct2r  11959  opnssneib  12314  restbasg  12326  restopn2  12341  iscnp4  12376  cnss2  12385  cnconst2  12391  cnptopresti  12396  cnptoprest2  12398  neitx  12426  uptx  12432  txrest  12434  txdis1cn  12436  xmetres2  12537  xblss2ps  12562  blhalf  12566  blssps  12585  blss  12586  blssexps  12587  blssex  12588  blin2  12590  metequiv2  12654  bdmetval  12658  metcnp3  12669  metcnp  12670  metcn  12672  metcnpi  12673  metcnpi2  12674  txmetcnp  12676  txmetcn  12677  qtopbas  12680  tgqioo  12705  fsumcncntop  12714  elcncf2  12719  mulcncflem  12748  mulcncf  12749  suplociccreex  12760  limcdifap  12789  cnplimcim  12794  cnplimccntop  12797  limccnpcntop  12802  dvcj  12831  dveflem  12844  sin0pilem1  12851  ptolemy  12894  coseq0q4123  12904  coseq0negpitopi  12906  cos02pilt1  12921  pwle2  13182  pwf1oexmid  13183  subctctexmid  13185  peano4nninf  13189  nninfalllemn  13191  nninfalllem1  13192  nninfall  13193  nninfsellemeq  13199  nninfsellemqall  13200  sbthom  13210  refeq  13212  isomninnlem  13214  trilpolemeq1  13222  trilpolemlt1  13223