Theorem simplr 528

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 489	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  1061  simp2lr  1065  simp3lr  1069  bilukdc  1396  dcun  3533  intab  3872  exmid01  4196  exmidundif  4204  exmidundifim  4205  frirrg  4348  reg2exmidlema  4531  imadiflem  5292  fvco4  5585  fvmptt  5604  fcoconst  5684  f1imass  5770  fcof1  5779  fliftfun  5792  riotass2  5852  ovmpodxf  5995  dftpos4  6259  tfrlem1  6304  tfrlem3ag  6305  tfrlemibacc  6322  tfrlemibfn  6324  tfrlemi1  6328  tfrlemi14d  6329  tfr1onlem3ag  6333  tfr1onlembacc  6338  tfr1onlembfn  6340  tfr1onlemaccex  6344  tfrcllembacc  6351  tfrcllembfn  6353  tfrcllemaccex  6357  frecabcl  6395  nntr2  6499  dcdifsnid  6500  nnm00  6526  ecopovsymg  6629  ecopoverg  6631  th3qlem1  6632  mapss  6686  f1imaen2g  6788  xpen  6840  xpmapenlem  6844  phpm  6860  fidifsnen  6865  dif1enen  6875  fiunsnnn  6876  fin0  6880  fin0or  6881  findcard2d  6886  findcard2sd  6887  diffifi  6889  isinfinf  6892  tridc  6894  fimax2gtrilemstep  6895  fimax2gtri  6896  en2eqpr  6902  onunsnss  6911  unsnfidcex  6914  unsnfidcel  6915  undifdcss  6917  unfiin  6920  fisseneq  6926  ssfirab  6928  f1finf1o  6941  fidcenumlemrks  6947  fidcenumlemrk  6948  fidcenumlemr  6949  fidcenum  6950  suplub2ti  6995  supisolem  7002  ordiso2  7029  djudom  7087  omp1eomlem  7088  difinfsnlem  7093  difinfinf  7095  ctm  7103  ctssdclemn0  7104  enumct  7109  nnnninfeq  7121  nnnninfeq2  7122  nninfisol  7126  enomnilem  7131  finomni  7133  exmidomni  7135  fodju0  7140  ismkvnex  7148  enmkvlem  7154  enwomnilem  7162  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  exmidaclem  7202  exmidontriimlem1  7215  exmidontriimlem2  7216  exmidontriimlem3  7217  exmidontriimlem4  7218  exmidontriim  7219  netap  7248  exmidapne  7254  dfplpq2  7348  dfmpq2  7349  mulpipqqs  7367  nqpi  7372  distrnqg  7381  prarloclemarch  7412  enq0tr  7428  nqnq0pi  7432  nq0nn  7436  nnnq0lem1  7440  prarloclemup  7489  prarloclem3  7491  prarloclemcalc  7496  genplt2i  7504  addnqprllem  7521  addnqprulem  7522  appdivnq  7557  distrlem1prl  7576  distrlem1pru  7577  ltaddpr  7591  ltexprlemlol  7596  ltexprlemupu  7598  ltexprlemdisj  7600  addcanprleml  7608  ltaprlem  7612  addextpr  7615  recexprlemopu  7621  recexprlemdisj  7624  recexprlem1ssl  7627  aptiprleml  7633  cauappcvgprlemm  7639  cauappcvgprlemopl  7640  cauappcvgprlemlol  7641  cauappcvgprlemopu  7642  cauappcvgprlemdisj  7645  cauappcvgprlemladdfu  7648  cauappcvgprlemladdfl  7649  cauappcvgprlemladdru  7650  cauappcvgprlemladdrl  7651  caucvgprlemm  7662  caucvgprlemopl  7663  caucvgprlemlol  7664  caucvgprlemopu  7665  caucvgprlemladdfu  7671  caucvgprprlemml  7688  caucvgprprlemopl  7691  caucvgprprlemlol  7692  caucvgprprlemopu  7693  caucvgprprlemexbt  7700  suplocexprlemru  7713  suplocexprlemloc  7715  suplocexprlemub  7717  suplocexprlemlub  7718  prsrlem1  7736  recexgt0sr  7767  mulgt0sr  7772  archsr  7776  caucvgsrlemcau  7787  caucvgsrlemoffcau  7792  caucvgsrlemoffres  7794  suplocsrlemb  7800  suplocsrlempr  7801  suplocsrlem  7802  addcnsr  7828  mulcnsr  7829  mulcnsrec  7837  axmulcom  7865  nntopi  7888  axcaucvglemcau  7892  axcaucvglemres  7893  axpre-suploclemres  7895  axpre-suploc  7896  axsuploc  8024  ltntri  8079  cnegexlem2  8127  cnegexlem3  8128  addsub4  8194  le2add  8395  lt2add  8396  lt2sub  8411  le2sub  8412  rereim  8537  apreim  8554  mulreim  8555  apcotr  8558  apadd1  8559  addext  8561  mulext1  8563  mulext  8565  apti  8573  aptap  8601  receuap  8620  rec11rap  8662  divdivdivap  8664  divadddivap  8678  divsubdivap  8679  rerecclap  8681  recgt0  8801  prodgt0gt0  8802  prodgt0  8803  prodge0  8805  lemulge11  8817  lt2mul2div  8830  ltrec  8834  lerec  8835  ltrec1  8839  lediv2a  8846  mulle0r  8895  sup3exmid  8908  zdiv  9335  eluzuzle  9530  supinfneg  9589  infsupneg  9590  infregelbex  9592  xrltso  9790  xnn0dcle  9796  xnn0letri  9797  npnflt  9809  nmnfgt  9812  z2ge  9820  xaddf  9838  xaddval  9839  xpncan  9865  xleadd1a  9867  xltadd1  9870  xaddge0  9872  xle2add  9873  xleaddadd  9881  ixxss1  9898  ixxss2  9899  elico2  9931  iccsupr  9960  fzass4  10055  fzrev  10077  fz0fzelfz0  10120  fzocatel  10192  elfzomelpfzo  10224  exbtwnzlemstep  10241  rebtwn2zlemstep  10246  qbtwnxr  10251  apbtwnz  10267  btwnzge0  10293  modqid  10342  modqcyc  10352  modqcyc2  10353  modqaddabs  10355  modqaddmod  10356  mulqaddmodid  10357  modqmuladd  10359  modqltm1p1mod  10369  modqsubmod  10375  modqsubmodmod  10376  modaddmodlo  10381  modqmulmod  10382  modqmulmodr  10383  modqsubdir  10386  addmodlteq  10391  iseqf1olemab  10482  iseqf1olemmo  10485  iseqf1olemjpcl  10488  iseqf1olemqpcl  10489  exp3val  10515  expcl2lemap  10525  expap0  10543  expnegzap  10547  expmul  10558  leexp1a  10568  qsqeqor  10623  expnbnd  10636  nn0ltexp2  10681  nn0opth2  10695  facndiv  10710  faclbnd  10712  bcval5  10734  bcpasc  10737  hashennnuni  10750  hashunlem  10775  hashunsng  10778  hashprg  10779  fiprsshashgt1  10788  hashxp  10797  fimaxq  10798  zfz1isolemiso  10810  zfz1isolem1  10811  seq3coll  10813  shftlem  10816  shftfvalg  10818  shftfval  10821  2shfti  10831  caucvgrelemrec  10979  caucvgrelemcau  10980  caucvgre  10981  cvg1nlemcau  10984  cvg1nlemres  10985  resqrexlemcalc3  11016  resqrexlemcvg  11019  resqrexlemglsq  11022  resqrexlemga  11023  sqrtsq  11044  leabs  11074  absexpzap  11080  abslt  11088  absle  11089  abssubap0  11090  caubnd2  11117  icodiamlt  11180  maxleim  11205  maxabslemval  11208  maxleastlt  11215  rexico  11221  zmaxcl  11224  fimaxre2  11226  minmax  11229  xrmaxleim  11243  xrmaxiflemcl  11244  xrmaxifle  11245  xrmaxiflemlub  11247  xrmaxiflemval  11249  xrmaxleastlt  11255  xrmaxltsup  11257  xrmaxadd  11260  xrminmax  11264  xrbdtri  11275  climuni  11292  climshftlemg  11301  iserex  11338  climcau  11346  climrecvg1n  11347  climcvg1nlem  11348  sumeq2  11358  summodclem3  11379  zsumdc  11383  isumss  11390  fisumss  11391  sumsnf  11408  fsumconst  11453  modfsummod  11457  fsum00  11461  fsumabs  11464  fsumrelem  11470  fsumiun  11476  isumsplit  11490  divcnv  11496  geo2sum  11513  geoisumr  11517  cvgratz  11531  ntrivcvgap  11547  prodeq2  11556  prodmodclem2  11576  prodmodc  11577  zproddc  11578  fprodmul  11590  prodsnf  11591  fprodcl2lem  11604  fprodconst  11619  fprodap0  11620  fprodrec  11628  fprodap0f  11635  fprodle  11639  fprodmodd  11640  tanaddap  11738  zdvdsdc  11810  dvds2ln  11822  dvdsle  11840  dvdsext  11851  divalglemeunn  11916  divalglemex  11917  divalglemeuneg  11918  zsupcllemstep  11936  dvdsbnd  11947  gcdsupex  11948  gcdsupcl  11949  dvdslegcd  11955  bezoutlemnewy  11987  bezoutlemstep  11988  bezoutlemmain  11989  bezoutlemzz  11993  bezoutlembz  11995  bezoutlembi  11996  bezoutlemle  11999  dfgcd3  12001  bezout  12002  dfgcd2  12005  dvdsmulgcd  12016  bezoutr  12023  uzwodc  12028  lcmval  12053  lcmcllem  12057  lcmneg  12064  ncoprmgcdne1b  12079  isprm2lem  12106  prmind2  12110  dvdsnprmd  12115  isprm5  12132  prmdvdsexp  12138  sqrt2irr  12152  oddpwdclemxy  12159  oddpwdclemdc  12163  nonsq  12197  pceu  12285  pcmul  12291  pc2dvds  12319  pcz  12321  pcprmpw2  12322  dvdsprmpweqle  12326  pcfac  12338  qexpz  12340  prmpwdvds  12343  1arith  12355  mul4sq  12382  ennnfonelemkh  12403  ennnfonelemhf1o  12404  ennnfonelemhom  12406  ennnfonelemfun  12408  ennnfonelemf1  12409  ennnfonelemim  12415  exmidunben  12417  ctiunctlemfo  12430  omiunct  12435  ssnnctlemct  12437  isstruct2r  12463  ismgm  12706  issgrp  12739  sgrpidmndm  12751  mndpropd  12771  issubmnd  12773  isgrpinv  12854  grplmulf1o  12872  dfgrp3mlem  12896  grplactcnv  12900  mhmid  12907  mhmmnd  12908  ghmgrp  12910  mulgval  12914  mulgfng  12915  mulgnnp1  12919  mulgnn0dir  12940  mulgneg2  12944  mhmmulg  12951  grpissubg  12980  issrg  13048  srglmhm  13076  srgrmhm  13077  isring  13083  ringadd2  13110  oppr1g  13151  reldvdsrsrg  13160  dvdsrvald  13161  dvdsrd  13162  dvdsrex  13166  dvdsrmul1  13170  unitgrp  13184  opnssneib  13438  restbasg  13450  restopn2  13465  iscnp4  13500  cnss2  13509  cnconst2  13515  cnptopresti  13520  cnptoprest2  13522  neitx  13550  uptx  13556  txrest  13558  txdis1cn  13560  xmetres2  13661  xblss2ps  13686  blhalf  13690  blssps  13709  blss  13710  blssexps  13711  blssex  13712  blin2  13714  metequiv2  13778  bdmetval  13782  metcnp3  13793  metcnp  13794  metcn  13796  metcnpi  13797  metcnpi2  13798  txmetcnp  13800  txmetcn  13801  qtopbas  13804  tgqioo  13829  fsumcncntop  13838  elcncf2  13843  mulcncflem  13872  mulcncf  13873  suplociccreex  13884  limcdifap  13913  cnplimcim  13918  cnplimccntop  13921  limccnpcntop  13926  dvcj  13955  dveflem  13969  reeff1olem  13974  eflt  13978  sin0pilem1  13984  ptolemy  14027  coseq0q4123  14037  coseq0negpitopi  14039  cos02pilt1  14054  cos11  14056  ioocosf1o  14057  cxplt  14118  cxple  14119  cxplt3  14122  apcxp2  14140  rprelogbmul  14155  rprelogbdiv  14157  lgsval  14187  lgsfcl2  14189  lgscllem  14190  lgsval2lem  14193  lgsdir2lem4  14214  lgsdir2lem5  14215  lgsdir2  14216  lgsne0  14221  2sqlem6  14238  2sqlem10  14243  pwle2  14519  pwf1oexmid  14520  subctctexmid  14521  pw1nct  14523  peano4nninf  14526  nninfalllem1  14528  nninfall  14529  nninfsellemeq  14534  nninfsellemqall  14535  sbthom  14545  refeq  14547  isomninnlem  14549  trilpolemeq1  14559  trilpolemlt1  14560  trirec0  14563  apdiff  14567  iswomninnlem  14568  ismkvnnlem  14571  redcwlpolemeq1  14573  ltlenmkv  14588