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  3082  disjiun  4029  isotr  5864  riota5f  5903  tfrexlem  6393  tfrcl  6423  nnsucuniel  6554  pw2f1odclem  6896  fopwdom  6898  dif1enen  6942  fisbth  6945  fin0  6947  fin0or  6948  diffisn  6955  finexdc  6964  fientri3  6977  unfidisj  6984  undifdc  6986  ssfirab  6998  fnfi  7003  iunfidisj  7013  dcfi  7048  ordiso2  7102  difinfinf  7168  ctmlemr  7175  exmidfodomrlemr  7271  2omotaplemap  7326  cc2lem  7335  cc3  7337  addcmpblnq  7436  mulcmpblnq  7437  ordpipqqs  7443  ltexnqq  7477  addcmpblnq0  7512  mulcmpblnq0  7513  prmu  7547  addlocpr  7605  prmuloc  7635  prmuloc2  7636  ltaddpr  7666  ltexprlemopl  7670  ltexprlemopu  7672  ltexprlemloc  7676  ltexprlemrl  7679  ltexprlemru  7681  addcanprleml  7683  addcanprlemu  7684  aptiprleml  7708  aptiprlemu  7709  ltmprr  7711  cauappcvgprlemloc  7721  archrecpr  7733  caucvgprlemloc  7744  caucvgprprlemloc  7772  caucvgprprlemexbt  7775  suplocexprlemdisj  7789  suplocexprlemloc  7790  addcmpblnr  7808  mulcmpblnrlemg  7809  mulcmpblnr  7810  ltsrprg  7816  mulgt0sr  7847  caucvgsrlemgt1  7864  suplocsrlemb  7875  axmulcl  7935  axarch  7960  axcaucvglemres  7968  axpre-suploclemres  7970  axpre-suploc  7971  readdcan  8168  cnegexlem1  8203  negeu  8219  add20  8503  apreap  8616  cru  8631  apsym  8635  apcotr  8636  apadd1  8637  apneg  8640  mulext1  8641  divdivdivap  8742  ltmul12a  8889  lemul12a  8891  lt2mul2div  8908  ledivdiv  8919  lediv12a  8923  qapne  9715  xleadd1a  9950  ixxss12  9983  ioodisj  10070  fz0fzelfz0  10204  zsupcllemstep  10321  zsupssdc  10330  qtri3or  10332  exbtwnzlemstep  10339  exbtwnzlemex  10341  exbtwnz  10342  rebtwn2zlemstep  10344  rebtwn2z  10346  qbtwnre  10348  btwnzge0  10392  iseqf1olemqf1o  10600  mulexpzap  10673  leexp1a  10688  expnbnd  10757  hashen  10878  fihashdom  10897  hashun  10899  zfz1iso  10935  cjap  11073  cvg1nlemres  11152  rsqrmo  11194  abs3lem  11278  cau3lem  11281  rexanre  11387  xrmaxltsup  11425  climcau  11514  sumeq2  11526  summodc  11550  fsum3cvg3  11563  fsum2d  11602  prodeq2  11724  prodmodclem2  11744  fprod2d  11790  eirrap  11945  addmodlteqALT  12026  divalglemeunn  12088  divalglemeuneg  12090  bezoutlemnewy  12173  bezoutlemstep  12174  bezoutlemmain  12175  bezoutlembi  12182  bezoutlemeu  12184  rpdvds  12277  isprm5lem  12319  isprm6  12325  pw2dvdslemn  12343  pw2dvdseu  12346  sqrt2irrap  12358  pythagtriplem2  12445  pythagtrip  12462  pclemub  12466  pcqmul  12482  pcexp  12488  pcneg  12504  pcprmpw2  12512  pcadd  12519  pcmpt  12522  4sqlem13m  12582  ennnfonelemrnh  12643  ennnfonelemnn0  12649  ctinfomlemom  12654  ctiunctlemfo  12666  nninfdclemf1  12679  imasival  12959  gsumpropd2  13046  sgrppropd  13066  ismndd  13088  mndpropd  13091  mhmeql  13134  mhmmnd  13256  issubg4m  13333  ssnmz  13351  conjnmzb  13420  rngpropd  13521  ringpropd  13604  islmod  13857  psrval  14230  restbasg  14414  cnrest2  14482  cnpdis  14488  lmtopcnp  14496  txcnp  14517  txlm  14525  ismet2  14600  blininf  14670  metss2lem  14743  xmettxlem  14755  xmettx  14756  metcnp3  14757  metcnpi3  14763  addcncntoplem  14807  fsumcncntop  14813  mulcncf  14854  dedekindeulemuub  14863  dedekindeu  14869  dedekindicclemuub  14872  ivthinclemlopn  14882  ivthinclemuopn  14884  ivthinclemloc  14887  ivthinc  14889  ivthdichlem  14897  limcimo  14911  limccnp2cntop  14923  plyf  14983  plyco  15005  plycj  15007  plyrecj  15009  dvply2g  15012  logbgcd1irrap  15216  perfectlem2  15246  lgsdilem  15278  lgsquad2lem2  15333  lgsquad3  15335  2sqlem5  15370  2sqlem9  15375  qdencn  15681  apdiff  15702