Theorem simpllr 540

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp-4r  548  f1o2ndf1  6468  tfrlem1  6584  tfr1onlemaccex  6624  tfrcllemaccex  6637  frecabcl  6675  fopwdom  7142  phplem4dom  7169  phpm  7173  phplem4on  7175  fidifsnen  7178  diffisn  7203  diffifi  7204  en2eqpr  7220  fisseneq  7248  suplub2ti  7347  difinfsn  7446  ctmlemr  7454  ctm  7455  ctssdclemn0  7456  ctssdc  7459  nninfninc  7469  nninfisol  7479  enomnilem  7484  enmkvlem  7507  enwomnilem  7515  nninfwlpoimlemginf  7522  exmidontriimlem4  7586  exmidontriim  7587  cc3  7640  addcmpblnq  7740  mulcmpblnq  7741  ordpipqqs  7747  ltexnqq  7781  enq0tr  7807  addcmpblnq0  7816  mulcmpblnq0  7817  nnnq0lem1  7819  prssnqu  7853  prarloclemup  7868  nqprl  7924  nqpru  7925  mullocpr  7944  cauappcvgprlemladdfu  8027  cauappcvgprlemladdrl  8030  caucvgprlemm  8041  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprlemlim  8054  caucvgprprlemml  8067  caucvgprprlemloc  8076  caucvgprprlemlim  8084  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  addcmpblnr  8112  mulcmpblnrlemg  8113  mulcmpblnr  8114  ltsrprg  8120  srpospr  8156  caucvgsrlemoffres  8173  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axcaucvglemcau  8271  axsuploc  8404  cnegexlem3  8510  negeu  8524  add20  8809  rimul  8921  apreap  8923  cru  8938  apreim  8939  apsym  8942  apcotr  8943  apadd1  8944  apneg  8947  mulext1  8948  apti  8958  aptap  8986  mulap0  8990  prodgt0  9190  ltmul12a  9198  ledivdiv  9228  lediv12a  9232  supinfneg  10010  infsupneg  10011  qapne  10054  irraddap  10062  xaddf  10262  xaddval  10263  xleadd1a  10291  xleaddadd  10305  ixxss12  10324  ioodisj  10411  fznlem  10461  zsupcllemstep  10678  qtri3or  10691  exbtwnzlemstep  10698  rebtwn2zlemstep  10703  addmodlteq  10855  seqf1og  10978  mulexpzap  11036  leexp1a  11051  expnbnd  11121  apexp1  11177  faclbnd  11200  hashxp  11288  sshashneg  11302  hashf1lem2  11307  zfz1iso  11314  swrdswrdlem  11497  cjap  11693  caucvgre  11768  cvg1nlemres  11772  resqrexlemglsq  11809  resqrexlemga  11810  sqrtsq  11831  ltabs  11875  abs3lem  11899  cau3lem  11902  maxleim  11993  rexico  12009  fiidxsupcl  12017  minmax  12019  xrmaxleim  12034  xrmaxiflemcl  12035  xrmaxiflemlub  12038  xrmaxiflemval  12040  xrmaxltsup  12048  xrmaxadd  12051  xrminmax  12055  xrbdtri  12066  climcau  12137  climrecvg1n  12138  sumeq2  12149  summodclem2  12173  divcnv  12288  prodeq2  12348  fprodsplitdc  12387  fprodconst  12411  dvdsle  12635  bitsfzo  12746  dvdsbnd  12757  bezoutlemmain  12799  bezoutlemzz  12803  bezoutlembi  12806  dfgcd3  12811  dvdsmulgcd  12826  nnmindc  12835  lcmcllem  12869  lcmgcdlem  12879  ncoprmgcdne1b  12891  isprm5  12945  pwbdvdslemn  12968  nnmaxpwlemparts  12976  pythagtriplem2  13073  pythagtrip  13090  pceu  13102  pc2dvds  13137  pcz  13139  pcadd  13147  pcfac  13157  exmidunben  13374  ctiunctlemfo  13387  unct  13390  sgrppropd  13786  sgrpidmndm  13791  mndpropd  13811  mhmeql  13857  isgrpinv  13917  dfgrp3mlem  13961  mhmmnd  13977  conjnmzb  14141  resscntz  14165  ghmcmn  14220  gzsumconst  14232  prdsval  14279  isrng  14339  issrg  14375  isring  14410  dvdsrmul1  14517  aprlring  14708  issubassa2  15143  psrbagmaxlem1  15178  tgrest  15412  cnpnei  15462  cnss1  15469  cncnp  15473  ismet2  15597  metequiv2  15739  metcnp  15755  metcnp2  15756  metcnpi3  15760  fsumcncntop  15810  elcncf2  15817  cncfmet  15835  suplociccreex  15867  dedekindicclemicc  15875  ivthinclemlr  15880  ivthinclemur  15882  cnplimclemr  15912  limccnpcntop  15918  limccoap  15921  dvmptfsum  15968  elply2  15978  plyrecj  16006  logdivlt  16141  zprmlogbap  16235  mersenne  16314  lgsval2lem  16351  lgsquad3  16425  usgr1eop  16708  usgr1vr  16711  pw1ndom3  17242  nninfalllem1  17274  nnnninfex  17288  sbthom  17294  apdiff  17321