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  6313  tfrlem1  6393  tfr1onlemaccex  6433  tfrcllemaccex  6446  frecabcl  6484  fopwdom  6932  phplem4dom  6958  phpm  6961  phplem4on  6963  fidifsnen  6966  diffisn  6989  diffifi  6990  en2eqpr  7003  fisseneq  7030  suplub2ti  7102  difinfsn  7201  ctmlemr  7209  ctm  7210  ctssdclemn0  7211  ctssdc  7214  nninfninc  7224  nninfisol  7234  enomnilem  7239  enmkvlem  7262  enwomnilem  7270  nninfwlpoimlemginf  7277  exmidontriimlem4  7335  exmidontriim  7336  cc3  7379  addcmpblnq  7479  mulcmpblnq  7480  ordpipqqs  7486  ltexnqq  7520  enq0tr  7546  addcmpblnq0  7555  mulcmpblnq0  7556  nnnq0lem1  7558  prssnqu  7592  prarloclemup  7607  nqprl  7663  nqpru  7664  mullocpr  7683  cauappcvgprlemladdfu  7766  cauappcvgprlemladdrl  7769  caucvgprlemm  7780  caucvgprlemladdfu  7789  caucvgprlemladdrl  7790  caucvgprlemlim  7793  caucvgprprlemml  7806  caucvgprprlemloc  7815  caucvgprprlemlim  7823  suplocexprlemmu  7830  suplocexprlemru  7831  suplocexprlemdisj  7832  suplocexprlemloc  7833  addcmpblnr  7851  mulcmpblnrlemg  7852  mulcmpblnr  7853  ltsrprg  7859  srpospr  7895  caucvgsrlemoffres  7912  suplocsrlemb  7918  suplocsrlempr  7919  suplocsrlem  7920  axcaucvglemcau  8010  axsuploc  8144  cnegexlem3  8248  negeu  8262  add20  8546  rimul  8657  apreap  8659  cru  8674  apreim  8675  apsym  8678  apcotr  8679  apadd1  8680  apneg  8683  mulext1  8684  apti  8694  aptap  8722  mulap0  8726  prodgt0  8924  ltmul12a  8932  ledivdiv  8962  lediv12a  8966  supinfneg  9715  infsupneg  9716  qapne  9759  xaddf  9965  xaddval  9966  xleadd1a  9994  xleaddadd  10008  ixxss12  10027  ioodisj  10114  fznlem  10162  zsupcllemstep  10370  qtri3or  10381  exbtwnzlemstep  10388  rebtwn2zlemstep  10393  addmodlteq  10541  seqf1og  10664  mulexpzap  10722  leexp1a  10737  expnbnd  10806  apexp1  10861  faclbnd  10884  hashxp  10969  zfz1iso  10984  cjap  11159  caucvgre  11234  cvg1nlemres  11238  resqrexlemglsq  11275  resqrexlemga  11276  sqrtsq  11297  ltabs  11340  abs3lem  11364  cau3lem  11367  maxleim  11458  rexico  11474  minmax  11483  xrmaxleim  11497  xrmaxiflemcl  11498  xrmaxiflemlub  11501  xrmaxiflemval  11503  xrmaxltsup  11511  xrmaxadd  11514  xrminmax  11518  xrbdtri  11529  climcau  11600  climrecvg1n  11601  sumeq2  11612  summodclem2  11635  divcnv  11750  prodeq2  11810  fprodsplitdc  11849  fprodconst  11873  dvdsle  12097  bitsfzo  12208  dvdsbnd  12219  bezoutlemmain  12261  bezoutlemzz  12265  bezoutlembi  12268  dfgcd3  12273  dvdsmulgcd  12288  nnmindc  12297  lcmcllem  12331  lcmgcdlem  12341  ncoprmgcdne1b  12353  isprm5  12406  pw2dvdslemn  12429  oddpwdclemxy  12433  pythagtriplem2  12531  pythagtrip  12548  pceu  12560  pc2dvds  12595  pcz  12597  pcadd  12605  pcfac  12615  exmidunben  12739  ctiunctlemfo  12752  unct  12755  prdsval  13047  sgrppropd  13187  sgrpidmndm  13194  mndpropd  13214  mhmeql  13266  isgrpinv  13328  dfgrp3mlem  13372  mhmmnd  13394  conjnmzb  13558  ghmcmn  13605  gsumfzconst  13619  isrng  13638  issrg  13669  isring  13704  reldvdsrsrg  13796  dvdsrmul1  13806  tgrest  14583  cnpnei  14633  cnss1  14640  cncnp  14644  ismet2  14768  metequiv2  14910  metcnp  14926  metcnp2  14927  metcnpi3  14931  fsumcncntop  14981  elcncf2  14988  cncfmet  15006  suplociccreex  15038  dedekindicclemicc  15046  ivthinclemlr  15051  ivthinclemur  15053  cnplimclemr  15083  limccnpcntop  15089  limccoap  15092  dvmptfsum  15139  elply2  15149  plyrecj  15177  mersenne  15411  lgsval2lem  15429  lgsquad3  15503  nninfalllem1  15878  nnnninfex  15892  sbthom  15898  apdiff  15920