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  6583  tfr1onlemaccex  6623  tfrcllemaccex  6636  frecabcl  6674  fopwdom  7140  phplem4dom  7167  phpm  7171  phplem4on  7173  fidifsnen  7176  diffisn  7201  diffifi  7202  en2eqpr  7218  fisseneq  7246  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  10011  infsupneg  10012  qapne  10055  irraddap  10063  xaddf  10263  xaddval  10264  xleadd1a  10292  xleaddadd  10306  ixxss12  10325  ioodisj  10412  fznlem  10462  zsupcllemstep  10679  qtri3or  10692  exbtwnzlemstep  10699  rebtwn2zlemstep  10704  addmodlteq  10856  seqf1og  10979  mulexpzap  11037  leexp1a  11052  expnbnd  11122  apexp1  11178  faclbnd  11201  hashxp  11289  sshashneg  11303  hashf1lem2  11308  zfz1iso  11315  swrdswrdlem  11498  cjap  11694  caucvgre  11769  cvg1nlemres  11773  resqrexlemglsq  11810  resqrexlemga  11811  sqrtsq  11832  ltabs  11876  abs3lem  11900  cau3lem  11903  maxleim  11994  rexico  12010  fiidxsupcl  12018  minmax  12020  xrmaxleim  12035  xrmaxiflemcl  12036  xrmaxiflemlub  12039  xrmaxiflemval  12041  xrmaxltsup  12049  xrmaxadd  12052  xrminmax  12056  xrbdtri  12067  climcau  12138  climrecvg1n  12139  sumeq2  12150  summodclem2  12174  divcnv  12289  prodeq2  12349  fprodsplitdc  12388  fprodconst  12412  dvdsle  12636  bitsfzo  12747  dvdsbnd  12758  bezoutlemmain  12800  bezoutlemzz  12804  bezoutlembi  12807  dfgcd3  12812  dvdsmulgcd  12827  nnmindc  12836  lcmcllem  12870  lcmgcdlem  12880  ncoprmgcdne1b  12892  isprm5  12946  pwbdvdslemn  12969  nnmaxpwlemparts  12977  pythagtriplem2  13074  pythagtrip  13091  pceu  13103  pc2dvds  13138  pcz  13140  pcadd  13148  pcfac  13158  exmidunben  13375  ctiunctlemfo  13388  unct  13391  sgrppropd  13787  sgrpidmndm  13792  mndpropd  13812  mhmeql  13858  isgrpinv  13918  dfgrp3mlem  13962  mhmmnd  13978  conjnmzb  14142  resscntz  14166  ghmcmn  14221  gzsumconst  14233  prdsval  14280  isrng  14340  issrg  14376  isring  14411  dvdsrmul1  14518  aprlring  14709  issubassa2  15144  tgrest  15395  cnpnei  15445  cnss1  15452  cncnp  15456  ismet2  15580  metequiv2  15722  metcnp  15738  metcnp2  15739  metcnpi3  15743  fsumcncntop  15793  elcncf2  15800  cncfmet  15818  suplociccreex  15850  dedekindicclemicc  15858  ivthinclemlr  15863  ivthinclemur  15865  cnplimclemr  15895  limccnpcntop  15901  limccoap  15904  dvmptfsum  15951  elply2  15961  plyrecj  15989  logdivlt  16124  zprmlogbap  16218  mersenne  16297  lgsval2lem  16334  lgsquad3  16408  usgr1eop  16691  usgr1vr  16694  pw1ndom3  17225  nninfalllem1  17257  nnnninfex  17271  sbthom  17277  apdiff  17304