Theorem simplrr 538

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  3125  disjiun  4083  isotr  5957  riota5f  5998  tfrexlem  6500  tfrcl  6530  nnsucuniel  6663  pw2f1odclem  7020  fopwdom  7022  dif1enen  7069  fisbth  7072  fin0  7074  fin0or  7075  diffisn  7082  fidcen  7088  finexdc  7092  elssdc  7094  fientri3  7107  unfidisj  7114  undifdc  7116  ssfirab  7129  fnfi  7135  iunfidisj  7145  dcfi  7180  ordiso2  7234  difinfinf  7300  ctmlemr  7307  exmidfodomrlemr  7413  2omotaplemap  7476  cc2lem  7485  cc3  7487  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  ltexnqq  7628  addcmpblnq0  7663  mulcmpblnq0  7664  prmu  7698  addlocpr  7756  prmuloc  7786  prmuloc2  7787  ltaddpr  7817  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  aptiprleml  7859  aptiprlemu  7860  ltmprr  7862  cauappcvgprlemloc  7872  archrecpr  7884  caucvgprlemloc  7895  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  suplocexprlemdisj  7940  suplocexprlemloc  7941  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  ltsrprg  7967  mulgt0sr  7998  caucvgsrlemgt1  8015  suplocsrlemb  8026  axmulcl  8086  axarch  8111  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  readdcan  8319  cnegexlem1  8354  negeu  8370  add20  8654  apreap  8767  cru  8782  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  divdivdivap  8893  ltmul12a  9040  lemul12a  9042  lt2mul2div  9059  ledivdiv  9070  lediv12a  9074  qapne  9873  xleadd1a  10108  ixxss12  10141  ioodisj  10228  fz0fzelfz0  10362  zsupcllemstep  10489  zsupssdc  10498  qtri3or  10500  exbtwnzlemstep  10507  exbtwnzlemex  10509  exbtwnz  10510  rebtwn2zlemstep  10512  rebtwn2z  10514  qbtwnre  10516  btwnzge0  10560  iseqf1olemqf1o  10768  mulexpzap  10841  leexp1a  10856  expnbnd  10925  hashen  11046  fihashdom  11066  hashun  11068  zfz1iso  11105  swrdccat  11316  reuccatpfxs1  11328  cjap  11467  cvg1nlemres  11546  rsqrmo  11588  abs3lem  11672  cau3lem  11675  rexanre  11781  xrmaxltsup  11819  climcau  11908  sumeq2  11920  summodc  11945  fsum3cvg3  11958  fsum2d  11997  prodeq2  12119  prodmodclem2  12139  fprod2d  12185  eirrap  12340  addmodlteqALT  12421  divalglemeunn  12483  divalglemeuneg  12485  bezoutlemnewy  12568  bezoutlemstep  12569  bezoutlemmain  12570  bezoutlembi  12577  bezoutlemeu  12579  rpdvds  12672  isprm5lem  12714  isprm6  12720  pw2dvdslemn  12738  pw2dvdseu  12741  sqrt2irrap  12753  pythagtriplem2  12840  pythagtrip  12857  pclemub  12861  pcqmul  12877  pcexp  12883  pcneg  12899  pcprmpw2  12907  pcadd  12914  pcmpt  12917  4sqlem13m  12977  ennnfonelemrnh  13038  ennnfonelemnn0  13044  ctinfomlemom  13049  ctiunctlemfo  13061  nninfdclemf1  13074  imasival  13390  gsumpropd2  13477  sgrppropd  13497  ismndd  13521  mndpropd  13524  mhmeql  13576  mhmmnd  13704  issubg4m  13781  ssnmz  13799  conjnmzb  13868  rngpropd  13970  ringpropd  14053  islmod  14307  psrval  14682  restbasg  14894  cnrest2  14962  cnpdis  14968  lmtopcnp  14976  txcnp  14997  txlm  15005  ismet2  15080  blininf  15150  metss2lem  15223  xmettxlem  15235  xmettx  15236  metcnp3  15237  metcnpi3  15243  addcncntoplem  15287  fsumcncntop  15293  mulcncf  15334  dedekindeulemuub  15343  dedekindeu  15349  dedekindicclemuub  15352  ivthinclemlopn  15362  ivthinclemuopn  15364  ivthinclemloc  15367  ivthinc  15369  ivthdichlem  15377  limcimo  15391  limccnp2cntop  15403  plyf  15463  plyco  15485  plycj  15487  plyrecj  15489  dvply2g  15492  logbgcd1irrap  15696  perfectlem2  15726  lgsdilem  15758  lgsquad2lem2  15813  lgsquad3  15815  2sqlem5  15850  2sqlem9  15855  usgredg4  16068  usgr1vr  16101  subuhgr  16125  subumgr  16127  clwwlknonex2lem2  16291  2omap  16597  qdencn  16634  apdiff  16655  gfsumval  16683