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  6314  tfrlem1  6394  tfr1onlemaccex  6434  tfrcllemaccex  6447  frecabcl  6485  fopwdom  6933  phplem4dom  6959  phpm  6962  phplem4on  6964  fidifsnen  6967  diffisn  6990  diffifi  6991  en2eqpr  7004  fisseneq  7031  suplub2ti  7103  difinfsn  7202  ctmlemr  7210  ctm  7211  ctssdclemn0  7212  ctssdc  7215  nninfninc  7225  nninfisol  7235  enomnilem  7240  enmkvlem  7263  enwomnilem  7271  nninfwlpoimlemginf  7278  exmidontriimlem4  7336  exmidontriim  7337  cc3  7380  addcmpblnq  7480  mulcmpblnq  7481  ordpipqqs  7487  ltexnqq  7521  enq0tr  7547  addcmpblnq0  7556  mulcmpblnq0  7557  nnnq0lem1  7559  prssnqu  7593  prarloclemup  7608  nqprl  7664  nqpru  7665  mullocpr  7684  cauappcvgprlemladdfu  7767  cauappcvgprlemladdrl  7770  caucvgprlemm  7781  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  caucvgprlemlim  7794  caucvgprprlemml  7807  caucvgprprlemloc  7816  caucvgprprlemlim  7824  suplocexprlemmu  7831  suplocexprlemru  7832  suplocexprlemdisj  7833  suplocexprlemloc  7834  addcmpblnr  7852  mulcmpblnrlemg  7853  mulcmpblnr  7854  ltsrprg  7860  srpospr  7896  caucvgsrlemoffres  7913  suplocsrlemb  7919  suplocsrlempr  7920  suplocsrlem  7921  axcaucvglemcau  8011  axsuploc  8145  cnegexlem3  8249  negeu  8263  add20  8547  rimul  8658  apreap  8660  cru  8675  apreim  8676  apsym  8679  apcotr  8680  apadd1  8681  apneg  8684  mulext1  8685  apti  8695  aptap  8723  mulap0  8727  prodgt0  8925  ltmul12a  8933  ledivdiv  8963  lediv12a  8967  supinfneg  9716  infsupneg  9717  qapne  9760  xaddf  9966  xaddval  9967  xleadd1a  9995  xleaddadd  10009  ixxss12  10028  ioodisj  10115  fznlem  10163  zsupcllemstep  10372  qtri3or  10383  exbtwnzlemstep  10390  rebtwn2zlemstep  10395  addmodlteq  10543  seqf1og  10666  mulexpzap  10724  leexp1a  10739  expnbnd  10808  apexp1  10863  faclbnd  10886  hashxp  10971  zfz1iso  10986  cjap  11217  caucvgre  11292  cvg1nlemres  11296  resqrexlemglsq  11333  resqrexlemga  11334  sqrtsq  11355  ltabs  11398  abs3lem  11422  cau3lem  11425  maxleim  11516  rexico  11532  minmax  11541  xrmaxleim  11555  xrmaxiflemcl  11556  xrmaxiflemlub  11559  xrmaxiflemval  11561  xrmaxltsup  11569  xrmaxadd  11572  xrminmax  11576  xrbdtri  11587  climcau  11658  climrecvg1n  11659  sumeq2  11670  summodclem2  11693  divcnv  11808  prodeq2  11868  fprodsplitdc  11907  fprodconst  11931  dvdsle  12155  bitsfzo  12266  dvdsbnd  12277  bezoutlemmain  12319  bezoutlemzz  12323  bezoutlembi  12326  dfgcd3  12331  dvdsmulgcd  12346  nnmindc  12355  lcmcllem  12389  lcmgcdlem  12399  ncoprmgcdne1b  12411  isprm5  12464  pw2dvdslemn  12487  oddpwdclemxy  12491  pythagtriplem2  12589  pythagtrip  12606  pceu  12618  pc2dvds  12653  pcz  12655  pcadd  12663  pcfac  12673  exmidunben  12797  ctiunctlemfo  12810  unct  12813  prdsval  13105  sgrppropd  13245  sgrpidmndm  13252  mndpropd  13272  mhmeql  13324  isgrpinv  13386  dfgrp3mlem  13430  mhmmnd  13452  conjnmzb  13616  ghmcmn  13663  gsumfzconst  13677  isrng  13696  issrg  13727  isring  13762  reldvdsrsrg  13854  dvdsrmul1  13864  tgrest  14641  cnpnei  14691  cnss1  14698  cncnp  14702  ismet2  14826  metequiv2  14968  metcnp  14984  metcnp2  14985  metcnpi3  14989  fsumcncntop  15039  elcncf2  15046  cncfmet  15064  suplociccreex  15096  dedekindicclemicc  15104  ivthinclemlr  15109  ivthinclemur  15111  cnplimclemr  15141  limccnpcntop  15147  limccoap  15150  dvmptfsum  15197  elply2  15207  plyrecj  15235  mersenne  15469  lgsval2lem  15487  lgsquad3  15561  nninfalllem1  15945  nnnninfex  15959  sbthom  15965  apdiff  15987