Theorem simplrr 526

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 109	. 2 |- ( ( ps /\ ch ) -> ch )
2	1	ad2antlr 481	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  rmob  3005  disjiun  3932  isotr  5725  riota5f  5762  tfrexlem  6239  tfrcl  6269  nnsucuniel  6399  fopwdom  6738  dif1enen  6782  fisbth  6785  fin0  6787  fin0or  6788  diffisn  6795  finexdc  6804  fientri3  6811  unfidisj  6818  undifdc  6820  ssfirab  6830  fnfi  6833  iunfidisj  6842  ordiso2  6928  difinfinf  6994  ctmlemr  7001  exmidfodomrlemr  7075  cc2lem  7098  cc3  7100  addcmpblnq  7199  mulcmpblnq  7200  ordpipqqs  7206  ltexnqq  7240  addcmpblnq0  7275  mulcmpblnq0  7276  prmu  7310  addlocpr  7368  prmuloc  7398  prmuloc2  7399  ltaddpr  7429  ltexprlemopl  7433  ltexprlemopu  7435  ltexprlemloc  7439  ltexprlemrl  7442  ltexprlemru  7444  addcanprleml  7446  addcanprlemu  7447  aptiprleml  7471  aptiprlemu  7472  ltmprr  7474  cauappcvgprlemloc  7484  archrecpr  7496  caucvgprlemloc  7507  caucvgprprlemloc  7535  caucvgprprlemexbt  7538  suplocexprlemdisj  7552  suplocexprlemloc  7553  addcmpblnr  7571  mulcmpblnrlemg  7572  mulcmpblnr  7573  ltsrprg  7579  mulgt0sr  7610  caucvgsrlemgt1  7627  suplocsrlemb  7638  axmulcl  7698  axarch  7723  axcaucvglemres  7731  axpre-suploclemres  7733  axpre-suploc  7734  readdcan  7926  cnegexlem1  7961  negeu  7977  add20  8260  apreap  8373  cru  8388  apsym  8392  apcotr  8393  apadd1  8394  apneg  8397  mulext1  8398  divdivdivap  8497  ltmul12a  8642  lemul12a  8644  lt2mul2div  8661  ledivdiv  8672  lediv12a  8676  qapne  9458  xleadd1a  9686  ixxss12  9719  ioodisj  9806  fz0fzelfz0  9935  qtri3or  10051  exbtwnzlemstep  10056  exbtwnzlemex  10058  exbtwnz  10059  rebtwn2zlemstep  10061  rebtwn2z  10063  qbtwnre  10065  btwnzge0  10104  iseqf1olemqf1o  10297  mulexpzap  10364  leexp1a  10379  expnbnd  10446  hashen  10562  fihashdom  10581  hashun  10583  zfz1iso  10616  cjap  10710  cvg1nlemres  10789  rsqrmo  10831  abs3lem  10915  cau3lem  10918  rexanre  11024  xrmaxltsup  11059  climcau  11148  sumeq2  11160  summodc  11184  fsum3cvg3  11197  fsum2d  11236  prodeq2  11358  prodmodclem2  11378  eirrap  11520  addmodlteqALT  11593  divalglemeunn  11654  divalglemeuneg  11656  zsupcllemstep  11674  bezoutlemnewy  11720  bezoutlemstep  11721  bezoutlemmain  11722  bezoutlembi  11729  bezoutlemeu  11731  rpdvds  11816  isprm6  11861  pw2dvdslemn  11879  pw2dvdseu  11882  sqrt2irrap  11894  ennnfonelemrnh  11965  ennnfonelemnn0  11971  ctinfomlemom  11976  ctiunctlemfo  11988  restbasg  12376  cnrest2  12444  cnpdis  12450  lmtopcnp  12458  txcnp  12479  txlm  12487  ismet2  12562  blininf  12632  metss2lem  12705  xmettxlem  12717  xmettx  12718  metcnp3  12719  metcnpi3  12725  addcncntoplem  12759  fsumcncntop  12764  mulcncf  12799  dedekindeulemuub  12803  dedekindeu  12809  dedekindicclemuub  12812  ivthinclemlopn  12822  ivthinclemuopn  12824  ivthinclemloc  12827  ivthinc  12829  limcimo  12842  limccnp2cntop  12854  logbgcd1irrap  13095  qdencn  13397  apdiff  13416