Theorem simplr 502

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  simp1lr  1028  simp2lr  1032  simp3lr  1036  bilukdc  1357  dcun  3439  intab  3766  exmid01  4081  exmidundif  4089  exmidundifim  4090  frirrg  4232  reg2exmidlema  4409  imadiflem  5160  fvco4  5447  fvmptt  5466  fcoconst  5545  f1imass  5629  fcof1  5638  fliftfun  5651  riotass2  5710  ovmpodxf  5850  dftpos4  6114  tfrlem1  6159  tfrlem3ag  6160  tfrlemibacc  6177  tfrlemibfn  6179  tfrlemi1  6183  tfrlemi14d  6184  tfr1onlem3ag  6188  tfr1onlembacc  6193  tfr1onlembfn  6195  tfr1onlemaccex  6199  tfrcllembacc  6206  tfrcllembfn  6208  tfrcllemaccex  6212  frecabcl  6250  nntr2  6353  dcdifsnid  6354  nnm00  6379  ecopovsymg  6482  ecopoverg  6484  th3qlem1  6485  mapss  6539  f1imaen2g  6641  xpen  6692  xpmapenlem  6696  phpm  6712  fidifsnen  6717  dif1enen  6727  fiunsnnn  6728  fin0  6732  fin0or  6733  findcard2d  6738  findcard2sd  6739  diffifi  6741  isinfinf  6744  tridc  6746  fimax2gtrilemstep  6747  fimax2gtri  6748  en2eqpr  6754  onunsnss  6758  unsnfidcex  6761  unsnfidcel  6762  undifdcss  6764  unfiin  6767  fisseneq  6773  ssfirab  6774  f1finf1o  6787  fidcenumlemrks  6793  fidcenumlemrk  6794  fidcenumlemr  6795  fidcenum  6796  suplub2ti  6840  supisolem  6847  ordiso2  6872  djudom  6930  omp1eomlem  6931  difinfsnlem  6936  difinfinf  6938  ctm  6946  ctssdclemn0  6947  enumct  6952  enomnilem  6960  finomni  6962  exmidomni  6964  fodju0  6969  ismkvnex  6979  exmidfodomrlemr  7006  exmidfodomrlemrALT  7007  exmidaclem  7012  dfplpq2  7110  dfmpq2  7111  mulpipqqs  7129  nqpi  7134  distrnqg  7143  prarloclemarch  7174  enq0tr  7190  nqnq0pi  7194  nq0nn  7198  nnnq0lem1  7202  prarloclemup  7251  prarloclem3  7253  prarloclemcalc  7258  genplt2i  7266  addnqprllem  7283  addnqprulem  7284  appdivnq  7319  distrlem1prl  7338  distrlem1pru  7339  ltaddpr  7353  ltexprlemlol  7358  ltexprlemupu  7360  ltexprlemdisj  7362  addcanprleml  7370  ltaprlem  7374  addextpr  7377  recexprlemopu  7383  recexprlemdisj  7386  recexprlem1ssl  7389  aptiprleml  7395  cauappcvgprlemm  7401  cauappcvgprlemopl  7402  cauappcvgprlemlol  7403  cauappcvgprlemopu  7404  cauappcvgprlemdisj  7407  cauappcvgprlemladdfu  7410  cauappcvgprlemladdfl  7411  cauappcvgprlemladdru  7412  cauappcvgprlemladdrl  7413  caucvgprlemm  7424  caucvgprlemopl  7425  caucvgprlemlol  7426  caucvgprlemopu  7427  caucvgprlemladdfu  7433  caucvgprprlemml  7450  caucvgprprlemopl  7453  caucvgprprlemlol  7454  caucvgprprlemopu  7455  caucvgprprlemexbt  7462  prsrlem1  7485  recexgt0sr  7516  mulgt0sr  7520  archsr  7524  caucvgsrlemcau  7535  caucvgsrlemoffcau  7540  caucvgsrlemoffres  7542  addcnsr  7569  mulcnsr  7570  mulcnsrec  7578  axmulcom  7606  nntopi  7629  axcaucvglemcau  7633  axcaucvglemres  7634  ltntri  7813  cnegexlem2  7861  cnegexlem3  7862  addsub4  7928  le2add  8125  lt2add  8126  lt2sub  8141  le2sub  8142  rereim  8266  apreim  8283  mulreim  8284  apcotr  8287  apadd1  8288  addext  8290  mulext1  8292  mulext  8294  apti  8302  receuap  8343  rec11rap  8384  divdivdivap  8386  divadddivap  8400  divsubdivap  8401  rerecclap  8403  recgt0  8518  prodgt0gt0  8519  prodgt0  8520  prodge0  8522  lemulge11  8534  lt2mul2div  8547  ltrec  8551  lerec  8552  ltrec1  8556  lediv2a  8563  mulle0r  8612  sup3exmid  8625  zdiv  9043  eluzuzle  9236  supinfneg  9292  infsupneg  9293  xrltso  9475  npnflt  9491  nmnfgt  9494  z2ge  9502  xaddf  9520  xaddval  9521  xpncan  9547  xleadd1a  9549  xltadd1  9552  xaddge0  9554  xle2add  9555  xleaddadd  9563  ixxss1  9580  ixxss2  9581  elico2  9613  iccsupr  9642  fzass4  9735  fzrev  9757  fz0fzelfz0  9797  fzocatel  9869  elfzomelpfzo  9901  exbtwnzlemstep  9918  rebtwn2zlemstep  9923  qbtwnxr  9928  apbtwnz  9940  btwnzge0  9966  modqid  10015  modqcyc  10025  modqcyc2  10026  modqaddabs  10028  modqaddmod  10029  mulqaddmodid  10030  modqmuladd  10032  modqltm1p1mod  10042  modqsubmod  10048  modqsubmodmod  10049  modaddmodlo  10054  modqmulmod  10055  modqmulmodr  10056  modqsubdir  10059  addmodlteq  10064  iseqf1olemab  10155  iseqf1olemmo  10158  iseqf1olemjpcl  10161  iseqf1olemqpcl  10162  exp3val  10188  expcl2lemap  10198  expap0  10216  expnegzap  10220  expmul  10231  leexp1a  10241  expnbnd  10308  nn0opth2  10363  facndiv  10378  faclbnd  10380  bcval5  10402  bcpasc  10405  hashennnuni  10418  hashunlem  10443  hashunsng  10446  hashprg  10447  fiprsshashgt1  10456  hashxp  10465  fimaxq  10466  zfz1isolemiso  10475  zfz1isolem1  10476  seq3coll  10478  shftlem  10481  shftfvalg  10483  shftfval  10486  2shfti  10496  caucvgrelemrec  10643  caucvgrelemcau  10644  caucvgre  10645  cvg1nlemcau  10648  cvg1nlemres  10649  resqrexlemcalc3  10680  resqrexlemcvg  10683  resqrexlemglsq  10686  resqrexlemga  10687  sqrtsq  10708  leabs  10738  absexpzap  10744  abslt  10752  absle  10753  abssubap0  10754  caubnd2  10781  icodiamlt  10844  maxleim  10869  maxabslemval  10872  maxleastlt  10879  rexico  10885  zmaxcl  10888  fimaxre2  10890  minmax  10893  xrmaxleim  10905  xrmaxiflemcl  10906  xrmaxifle  10907  xrmaxiflemlub  10909  xrmaxiflemval  10911  xrmaxleastlt  10917  xrmaxltsup  10919  xrmaxadd  10922  xrminmax  10926  xrbdtri  10937  climuni  10954  climshftlemg  10963  iserex  11000  climcau  11008  climrecvg1n  11009  climcvg1nlem  11010  sumeq2  11020  summodclem3  11041  zsumdc  11045  isumss  11052  fisumss  11053  sumsnf  11070  fsumconst  11115  modfsummod  11119  fsum00  11123  fsumabs  11126  fsumrelem  11132  fsumiun  11138  isumsplit  11152  divcnv  11158  geo2sum  11175  geoisumr  11179  cvgratz  11193  tanaddap  11297  zdvdsdc  11362  dvds2ln  11374  dvdsle  11390  dvdsext  11401  divalglemeunn  11466  divalglemex  11467  divalglemeuneg  11468  zsupcllemstep  11486  dvdsbnd  11493  gcdsupex  11494  gcdsupcl  11495  dvdslegcd  11501  bezoutlemnewy  11530  bezoutlemstep  11531  bezoutlemmain  11532  bezoutlemzz  11536  bezoutlembz  11538  bezoutlembi  11539  bezoutlemle  11542  dfgcd3  11544  bezout  11545  dfgcd2  11548  dvdsmulgcd  11559  bezoutr  11566  lcmval  11590  lcmcllem  11594  lcmneg  11601  ncoprmgcdne1b  11616  isprm2lem  11643  prmind2  11647  dvdsnprmd  11652  prmdvdsexp  11672  sqrt2irr  11686  oddpwdclemxy  11692  oddpwdclemdc  11696  nonsq  11730  ennnfonelemkh  11770  ennnfonelemhf1o  11771  ennnfonelemhom  11773  ennnfonelemfun  11775  ennnfonelemf1  11776  ennnfonelemim  11782  exmidunben  11784  ctiunctlemfo  11795  isstruct2r  11813  opnssneib  12168  restbasg  12180  restopn2  12195  iscnp4  12229  cnss2  12238  cnconst2  12244  cnptopresti  12249  cnptoprest2  12251  neitx  12279  uptx  12285  txrest  12287  txdis1cn  12289  xmetres2  12368  xblss2ps  12393  blhalf  12397  blssps  12416  blss  12417  blssexps  12418  blssex  12419  blin2  12421  metequiv2  12485  bdmetval  12489  metcnp3  12500  metcnp  12501  metcn  12503  metcnpi  12504  metcnpi2  12505  txmetcnp  12507  txmetcn  12508  qtopbas  12511  tgqioo  12533  fsumcncntop  12542  elcncf2  12547  mulcncflem  12576  mulcncf  12577  limcdifap  12587  cnplimcim  12592  cnplimccntop  12595  limccnpcntop  12600  pwle2  12885  pwf1oexmid  12886  subctctexmid  12888  peano4nninf  12892  nninfalllemn  12894  nninfalllem1  12895  nninfall  12896  nninfsellemeq  12902  nninfsellemqall  12903  sbthom  12913  refeq  12915  isomninnlem  12917  trilpolemeq1  12925  trilpolemlt1  12926