Theorem simplrr 531

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 486	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  3047  disjiun  3984  isotr  5795  riota5f  5833  tfrexlem  6313  tfrcl  6343  nnsucuniel  6474  fopwdom  6814  dif1enen  6858  fisbth  6861  fin0  6863  fin0or  6864  diffisn  6871  finexdc  6880  fientri3  6892  unfidisj  6899  undifdc  6901  ssfirab  6911  fnfi  6914  iunfidisj  6923  dcfi  6958  ordiso2  7012  difinfinf  7078  ctmlemr  7085  exmidfodomrlemr  7179  cc2lem  7228  cc3  7230  addcmpblnq  7329  mulcmpblnq  7330  ordpipqqs  7336  ltexnqq  7370  addcmpblnq0  7405  mulcmpblnq0  7406  prmu  7440  addlocpr  7498  prmuloc  7528  prmuloc2  7529  ltaddpr  7559  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemloc  7569  ltexprlemrl  7572  ltexprlemru  7574  addcanprleml  7576  addcanprlemu  7577  aptiprleml  7601  aptiprlemu  7602  ltmprr  7604  cauappcvgprlemloc  7614  archrecpr  7626  caucvgprlemloc  7637  caucvgprprlemloc  7665  caucvgprprlemexbt  7668  suplocexprlemdisj  7682  suplocexprlemloc  7683  addcmpblnr  7701  mulcmpblnrlemg  7702  mulcmpblnr  7703  ltsrprg  7709  mulgt0sr  7740  caucvgsrlemgt1  7757  suplocsrlemb  7768  axmulcl  7828  axarch  7853  axcaucvglemres  7861  axpre-suploclemres  7863  axpre-suploc  7864  readdcan  8059  cnegexlem1  8094  negeu  8110  add20  8393  apreap  8506  cru  8521  apsym  8525  apcotr  8526  apadd1  8527  apneg  8530  mulext1  8531  divdivdivap  8630  ltmul12a  8776  lemul12a  8778  lt2mul2div  8795  ledivdiv  8806  lediv12a  8810  qapne  9598  xleadd1a  9830  ixxss12  9863  ioodisj  9950  fz0fzelfz0  10083  qtri3or  10199  exbtwnzlemstep  10204  exbtwnzlemex  10206  exbtwnz  10207  rebtwn2zlemstep  10209  rebtwn2z  10211  qbtwnre  10213  btwnzge0  10256  iseqf1olemqf1o  10449  mulexpzap  10516  leexp1a  10531  expnbnd  10599  hashen  10718  fihashdom  10738  hashun  10740  zfz1iso  10776  cjap  10870  cvg1nlemres  10949  rsqrmo  10991  abs3lem  11075  cau3lem  11078  rexanre  11184  xrmaxltsup  11221  climcau  11310  sumeq2  11322  summodc  11346  fsum3cvg3  11359  fsum2d  11398  prodeq2  11520  prodmodclem2  11540  fprod2d  11586  eirrap  11740  addmodlteqALT  11819  divalglemeunn  11880  divalglemeuneg  11882  zsupcllemstep  11900  zsupssdc  11909  bezoutlemnewy  11951  bezoutlemstep  11952  bezoutlemmain  11953  bezoutlembi  11960  bezoutlemeu  11962  rpdvds  12053  isprm5lem  12095  isprm6  12101  pw2dvdslemn  12119  pw2dvdseu  12122  sqrt2irrap  12134  pythagtriplem2  12220  pythagtrip  12237  pclemub  12241  pcqmul  12257  pcexp  12263  pcneg  12278  pcprmpw2  12286  pcadd  12293  pcmpt  12295  ennnfonelemrnh  12371  ennnfonelemnn0  12377  ctinfomlemom  12382  ctiunctlemfo  12394  nninfdclemf1  12407  ismndd  12673  mndpropd  12676  mhmeql  12707  restbasg  12962  cnrest2  13030  cnpdis  13036  lmtopcnp  13044  txcnp  13065  txlm  13073  ismet2  13148  blininf  13218  metss2lem  13291  xmettxlem  13303  xmettx  13304  metcnp3  13305  metcnpi3  13311  addcncntoplem  13345  fsumcncntop  13350  mulcncf  13385  dedekindeulemuub  13389  dedekindeu  13395  dedekindicclemuub  13398  ivthinclemlopn  13408  ivthinclemuopn  13410  ivthinclemloc  13413  ivthinc  13415  limcimo  13428  limccnp2cntop  13440  logbgcd1irrap  13682  lgsdilem  13722  2sqlem5  13749  2sqlem9  13754  qdencn  14059  apdiff  14080