Theorem simpllr 534

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simpllr	|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )

Proof of Theorem simpllr

Step	Hyp	Ref	Expression
1		simpr 110	. 2 |- ( ( ph /\ ps ) -> ps )
2	1	ad2antrr 488	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> 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:  simp-4r  542  f1o2ndf1  6295  tfrlem1  6375  tfr1onlemaccex  6415  tfrcllemaccex  6428  frecabcl  6466  fopwdom  6906  phplem4dom  6932  phpm  6935  phplem4on  6937  fidifsnen  6940  diffisn  6963  diffifi  6964  en2eqpr  6977  fisseneq  7004  suplub2ti  7076  difinfsn  7175  ctmlemr  7183  ctm  7184  ctssdclemn0  7185  ctssdc  7188  nninfninc  7198  nninfisol  7208  enomnilem  7213  enmkvlem  7236  enwomnilem  7244  nninfwlpoimlemginf  7251  exmidontriimlem4  7307  exmidontriim  7308  cc3  7351  addcmpblnq  7451  mulcmpblnq  7452  ordpipqqs  7458  ltexnqq  7492  enq0tr  7518  addcmpblnq0  7527  mulcmpblnq0  7528  nnnq0lem1  7530  prssnqu  7564  prarloclemup  7579  nqprl  7635  nqpru  7636  mullocpr  7655  cauappcvgprlemladdfu  7738  cauappcvgprlemladdrl  7741  caucvgprlemm  7752  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  caucvgprlemlim  7765  caucvgprprlemml  7778  caucvgprprlemloc  7787  caucvgprprlemlim  7795  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemloc  7805  addcmpblnr  7823  mulcmpblnrlemg  7824  mulcmpblnr  7825  ltsrprg  7831  srpospr  7867  caucvgsrlemoffres  7884  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  axcaucvglemcau  7982  axsuploc  8116  cnegexlem3  8220  negeu  8234  add20  8518  rimul  8629  apreap  8631  cru  8646  apreim  8647  apsym  8650  apcotr  8651  apadd1  8652  apneg  8655  mulext1  8656  apti  8666  aptap  8694  mulap0  8698  prodgt0  8896  ltmul12a  8904  ledivdiv  8934  lediv12a  8938  supinfneg  9686  infsupneg  9687  qapne  9730  xaddf  9936  xaddval  9937  xleadd1a  9965  xleaddadd  9979  ixxss12  9998  ioodisj  10085  fznlem  10133  zsupcllemstep  10336  qtri3or  10347  exbtwnzlemstep  10354  rebtwn2zlemstep  10359  addmodlteq  10507  seqf1og  10630  mulexpzap  10688  leexp1a  10703  expnbnd  10772  apexp1  10827  faclbnd  10850  hashxp  10935  zfz1iso  10950  cjap  11088  caucvgre  11163  cvg1nlemres  11167  resqrexlemglsq  11204  resqrexlemga  11205  sqrtsq  11226  ltabs  11269  abs3lem  11293  cau3lem  11296  maxleim  11387  rexico  11403  minmax  11412  xrmaxleim  11426  xrmaxiflemcl  11427  xrmaxiflemlub  11430  xrmaxiflemval  11432  xrmaxltsup  11440  xrmaxadd  11443  xrminmax  11447  xrbdtri  11458  climcau  11529  climrecvg1n  11530  sumeq2  11541  summodclem2  11564  divcnv  11679  prodeq2  11739  fprodsplitdc  11778  fprodconst  11802  dvdsle  12026  bitsfzo  12137  dvdsbnd  12148  bezoutlemmain  12190  bezoutlemzz  12194  bezoutlembi  12197  dfgcd3  12202  dvdsmulgcd  12217  nnmindc  12226  lcmcllem  12260  lcmgcdlem  12270  ncoprmgcdne1b  12282  isprm5  12335  pw2dvdslemn  12358  oddpwdclemxy  12362  pythagtriplem2  12460  pythagtrip  12477  pceu  12489  pc2dvds  12524  pcz  12526  pcadd  12534  pcfac  12544  exmidunben  12668  ctiunctlemfo  12681  unct  12684  prdsval  12975  sgrppropd  13115  sgrpidmndm  13122  mndpropd  13142  mhmeql  13194  isgrpinv  13256  dfgrp3mlem  13300  mhmmnd  13322  conjnmzb  13486  ghmcmn  13533  gsumfzconst  13547  isrng  13566  issrg  13597  isring  13632  reldvdsrsrg  13724  dvdsrmul1  13734  tgrest  14489  cnpnei  14539  cnss1  14546  cncnp  14550  ismet2  14674  metequiv2  14816  metcnp  14832  metcnp2  14833  metcnpi3  14837  fsumcncntop  14887  elcncf2  14894  cncfmet  14912  suplociccreex  14944  dedekindicclemicc  14952  ivthinclemlr  14957  ivthinclemur  14959  cnplimclemr  14989  limccnpcntop  14995  limccoap  14998  dvmptfsum  15045  elply2  15055  plyrecj  15083  mersenne  15317  lgsval2lem  15335  lgsquad3  15409  nninfalllem1  15739  sbthom  15757  apdiff  15779