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  3135  disjiun  4103  isotr  5988  riota5f  6029  tfrexlem  6564  tfrcl  6594  nnsucuniel  6727  pw2f1odclem  7086  fopwdom  7088  dif1enen  7136  fisbth  7139  fin0  7141  fin0or  7142  diffisn  7149  fidcen  7155  finexdc  7159  elssdc  7161  fientri3  7174  unfidisj  7181  undifdc  7183  ssfirab  7196  fnfi  7202  iunfidisj  7212  mapfi  7213  fissfi  7215  dcfi  7267  2omap  7268  ordiso2  7325  difinfinf  7391  ctmlemr  7398  exmidfodomrlemr  7504  2omotaplemap  7570  cc2lem  7579  cc3  7581  addcmpblnq  7681  mulcmpblnq  7682  ordpipqqs  7688  ltexnqq  7722  addcmpblnq0  7757  mulcmpblnq0  7758  prmu  7792  addlocpr  7850  prmuloc  7880  prmuloc2  7881  ltaddpr  7911  ltexprlemopl  7915  ltexprlemopu  7917  ltexprlemloc  7921  ltexprlemrl  7924  ltexprlemru  7926  addcanprleml  7928  addcanprlemu  7929  aptiprleml  7953  aptiprlemu  7954  ltmprr  7956  cauappcvgprlemloc  7966  archrecpr  7978  caucvgprlemloc  7989  caucvgprprlemloc  8017  caucvgprprlemexbt  8020  suplocexprlemdisj  8034  suplocexprlemloc  8035  addcmpblnr  8053  mulcmpblnrlemg  8054  mulcmpblnr  8055  ltsrprg  8061  mulgt0sr  8092  caucvgsrlemgt1  8109  suplocsrlemb  8120  axmulcl  8180  axarch  8205  axcaucvglemres  8213  axpre-suploclemres  8215  axpre-suploc  8216  readdcan  8412  cnegexlem1  8447  negeu  8463  add20  8747  apreap  8860  cru  8875  apsym  8879  apcotr  8880  apadd1  8881  apneg  8884  mulext1  8885  divdivdivap  8986  ltmul12a  9133  lemul12a  9135  lt2mul2div  9152  ledivdiv  9163  lediv12a  9167  qapne  9970  xleadd1a  10205  ixxss12  10238  ioodisj  10325  fz0fzelfz0  10460  zsupcllemstep  10588  zsupssdc  10597  qtri3or  10599  exbtwnzlemstep  10606  exbtwnzlemex  10608  exbtwnz  10609  rebtwn2zlemstep  10611  rebtwn2z  10613  qbtwnre  10615  btwnzge0  10659  iseqf1olemqf1o  10867  mulexpzap  10940  leexp1a  10955  expnbnd  11024  hashen  11145  fihashdom  11165  hashun  11167  zfz1iso  11209  swrdccat  11423  reuccatpfxs1  11435  cjap  11587  cvg1nlemres  11666  rsqrmo  11708  abs3lem  11792  cau3lem  11795  rexanre  11901  xrmaxltsup  11939  climcau  12028  sumeq2  12040  summodc  12065  fsum3cvg3  12078  fsum2d  12117  prodeq2  12239  prodmodclem2  12259  fprod2d  12305  eirrap  12460  addmodlteqALT  12541  divalglemeunn  12603  divalglemeuneg  12605  bezoutlemnewy  12688  bezoutlemstep  12689  bezoutlemmain  12690  bezoutlembi  12697  bezoutlemeu  12699  rpdvds  12792  isprm5lem  12834  isprm6  12840  pw2dvdslemn  12858  pw2dvdseu  12861  sqrt2irrap  12873  pythagtriplem2  12960  pythagtrip  12977  pclemub  12981  pcqmul  12997  pcexp  13003  pcneg  13019  pcprmpw2  13027  pcadd  13034  pcmpt  13037  4sqlem13m  13097  ennnfonelemrnh  13159  ennnfonelemnn0  13165  ctinfomlemom  13170  ctiunctlemfo  13182  nninfdclemf1  13195  imasival  13511  gsumpropd2  13598  sgrppropd  13618  ismndd  13642  mndpropd  13645  mhmeql  13697  mhmmnd  13825  issubg4m  13902  ssnmz  13920  conjnmzb  13989  rngpropd  14091  ringpropd  14174  aprlring  14426  islmod  14431  psrval  14806  restbasg  15025  cnrest2  15093  cnpdis  15099  lmtopcnp  15107  txcnp  15128  txlm  15136  ismet2  15211  blininf  15281  metss2lem  15354  xmettxlem  15366  xmettx  15367  metcnp3  15368  metcnpi3  15374  addcncntoplem  15418  fsumcncntop  15424  mulcncf  15465  dedekindeulemuub  15474  dedekindeu  15480  dedekindicclemuub  15483  ivthinclemlopn  15493  ivthinclemuopn  15495  ivthinclemloc  15498  ivthinc  15500  ivthdichlem  15508  limcimo  15522  limccnp2cntop  15534  plyf  15594  plyco  15616  plycj  15618  plyrecj  15620  dvply2g  15623  logbgcd1irrap  15827  perfectlem2  15860  lgsdilem  15892  lgsquad2lem2  15947  lgsquad3  15949  2sqlem5  15984  2sqlem9  15989  usgredg4  16202  usgr1vr  16235  subuhgr  16259  subumgr  16261  clwwlknonex2lem2  16425  eupth2lemsfi  16465  depindlem3  16495  qdencn  16799  apdiff  16824  qdiff  16825  gfsumval  16853