Theorem simplrr 536

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

Assertion

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

Proof of Theorem simplrr

Step	Hyp	Ref	Expression
1		simpr 110	. 2 |- ( ( ps /\ ch ) -> ch )
2	1	ad2antlr 489	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ch )

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:  rmob  3093  disjiun  4043  isotr  5895  riota5f  5934  tfrexlem  6430  tfrcl  6460  nnsucuniel  6591  pw2f1odclem  6943  fopwdom  6945  dif1enen  6989  fisbth  6992  fin0  6994  fin0or  6995  diffisn  7002  finexdc  7011  fientri3  7024  unfidisj  7031  undifdc  7033  ssfirab  7045  fnfi  7050  iunfidisj  7060  dcfi  7095  ordiso2  7149  difinfinf  7215  ctmlemr  7222  exmidfodomrlemr  7323  2omotaplemap  7382  cc2lem  7391  cc3  7393  addcmpblnq  7493  mulcmpblnq  7494  ordpipqqs  7500  ltexnqq  7534  addcmpblnq0  7569  mulcmpblnq0  7570  prmu  7604  addlocpr  7662  prmuloc  7692  prmuloc2  7693  ltaddpr  7723  ltexprlemopl  7727  ltexprlemopu  7729  ltexprlemloc  7733  ltexprlemrl  7736  ltexprlemru  7738  addcanprleml  7740  addcanprlemu  7741  aptiprleml  7765  aptiprlemu  7766  ltmprr  7768  cauappcvgprlemloc  7778  archrecpr  7790  caucvgprlemloc  7801  caucvgprprlemloc  7829  caucvgprprlemexbt  7832  suplocexprlemdisj  7846  suplocexprlemloc  7847  addcmpblnr  7865  mulcmpblnrlemg  7866  mulcmpblnr  7867  ltsrprg  7873  mulgt0sr  7904  caucvgsrlemgt1  7921  suplocsrlemb  7932  axmulcl  7992  axarch  8017  axcaucvglemres  8025  axpre-suploclemres  8027  axpre-suploc  8028  readdcan  8225  cnegexlem1  8260  negeu  8276  add20  8560  apreap  8673  cru  8688  apsym  8692  apcotr  8693  apadd1  8694  apneg  8697  mulext1  8698  divdivdivap  8799  ltmul12a  8946  lemul12a  8948  lt2mul2div  8965  ledivdiv  8976  lediv12a  8980  qapne  9773  xleadd1a  10008  ixxss12  10041  ioodisj  10128  fz0fzelfz0  10262  zsupcllemstep  10385  zsupssdc  10394  qtri3or  10396  exbtwnzlemstep  10403  exbtwnzlemex  10405  exbtwnz  10406  rebtwn2zlemstep  10408  rebtwn2z  10410  qbtwnre  10412  btwnzge0  10456  iseqf1olemqf1o  10664  mulexpzap  10737  leexp1a  10752  expnbnd  10821  hashen  10942  fihashdom  10961  hashun  10963  zfz1iso  10999  cjap  11267  cvg1nlemres  11346  rsqrmo  11388  abs3lem  11472  cau3lem  11475  rexanre  11581  xrmaxltsup  11619  climcau  11708  sumeq2  11720  summodc  11744  fsum3cvg3  11757  fsum2d  11796  prodeq2  11918  prodmodclem2  11938  fprod2d  11984  eirrap  12139  addmodlteqALT  12220  divalglemeunn  12282  divalglemeuneg  12284  bezoutlemnewy  12367  bezoutlemstep  12368  bezoutlemmain  12369  bezoutlembi  12376  bezoutlemeu  12378  rpdvds  12471  isprm5lem  12513  isprm6  12519  pw2dvdslemn  12537  pw2dvdseu  12540  sqrt2irrap  12552  pythagtriplem2  12639  pythagtrip  12656  pclemub  12660  pcqmul  12676  pcexp  12682  pcneg  12698  pcprmpw2  12706  pcadd  12713  pcmpt  12716  4sqlem13m  12776  ennnfonelemrnh  12837  ennnfonelemnn0  12843  ctinfomlemom  12848  ctiunctlemfo  12860  nninfdclemf1  12873  imasival  13188  gsumpropd2  13275  sgrppropd  13295  ismndd  13319  mndpropd  13322  mhmeql  13374  mhmmnd  13502  issubg4m  13579  ssnmz  13597  conjnmzb  13666  rngpropd  13767  ringpropd  13850  islmod  14103  psrval  14478  restbasg  14690  cnrest2  14758  cnpdis  14764  lmtopcnp  14772  txcnp  14793  txlm  14801  ismet2  14876  blininf  14946  metss2lem  15019  xmettxlem  15031  xmettx  15032  metcnp3  15033  metcnpi3  15039  addcncntoplem  15083  fsumcncntop  15089  mulcncf  15130  dedekindeulemuub  15139  dedekindeu  15145  dedekindicclemuub  15148  ivthinclemlopn  15158  ivthinclemuopn  15160  ivthinclemloc  15163  ivthinc  15165  ivthdichlem  15173  limcimo  15187  limccnp2cntop  15199  plyf  15259  plyco  15281  plycj  15283  plyrecj  15285  dvply2g  15288  logbgcd1irrap  15492  perfectlem2  15522  lgsdilem  15554  lgsquad2lem2  15609  lgsquad3  15611  2sqlem5  15646  2sqlem9  15651  2omap  16047  qdencn  16081  apdiff  16102