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  3139  disjiun  4109  isotr  5995  riota5f  6038  tfrexlem  6578  tfrcl  6608  nnsucuniel  6741  pw2f1odclem  7100  fopwdom  7102  dif1enen  7150  fisbth  7153  fin0  7155  fin0or  7156  diffisn  7163  fidcen  7169  finexdc  7173  elssdc  7175  fientri3  7188  unfidisj  7195  undifdc  7197  ssfirab  7210  fnfi  7216  iunfidisj  7226  mapfi  7227  fissfi  7229  dcfi  7281  2omap  7282  ordiso2  7339  difinfinf  7405  ctmlemr  7412  exmidfodomrlemr  7518  2omotaplemap  7587  cc2lem  7596  cc3  7598  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  ltexnqq  7739  addcmpblnq0  7774  mulcmpblnq0  7775  prmu  7809  addlocpr  7867  prmuloc  7897  prmuloc2  7898  ltaddpr  7928  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemloc  7938  ltexprlemrl  7941  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  aptiprleml  7970  aptiprlemu  7971  ltmprr  7973  cauappcvgprlemloc  7983  archrecpr  7995  caucvgprlemloc  8006  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  suplocexprlemdisj  8051  suplocexprlemloc  8052  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  ltsrprg  8078  mulgt0sr  8109  caucvgsrlemgt1  8126  suplocsrlemb  8137  axmulcl  8197  axarch  8222  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  readdcan  8430  cnegexlem1  8465  negeu  8481  add20  8766  apreap  8879  cru  8894  apsym  8898  apcotr  8899  apadd1  8900  apneg  8903  mulext1  8904  divdivdivap  9007  ltmul12a  9154  lemul12a  9156  lt2mul2div  9173  ledivdiv  9184  lediv12a  9188  qapne  9992  xleadd1a  10228  ixxss12  10261  ioodisj  10348  fz0fzelfz0  10486  zsupcllemstep  10614  zsupssdc  10625  qtri3or  10627  exbtwnzlemstep  10634  exbtwnzlemex  10636  exbtwnz  10637  rebtwn2zlemstep  10639  rebtwn2z  10641  qbtwnre  10643  btwnzge0  10687  iseqf1olemqf1o  10895  mulexpzap  10968  leexp1a  10983  expnbnd  11053  hashen  11175  fihashdom  11195  hashun  11197  zfz1iso  11241  swrdccat  11455  reuccatpfxs1  11467  cjap  11620  cvg1nlemres  11699  rsqrmo  11741  abs3lem  11825  cau3lem  11828  rexanre  11934  xrmaxltsup  11972  climcau  12061  sumeq2  12073  summodc  12098  fsum3cvg3  12111  fsum2d  12150  prodeq2  12272  prodmodclem2  12292  fprod2d  12338  eirrap  12493  addmodlteqALT  12574  divalglemeunn  12636  divalglemeuneg  12638  bezoutlemnewy  12721  bezoutlemstep  12722  bezoutlemmain  12723  bezoutlembi  12730  bezoutlemeu  12732  rpdvds  12825  isprm5lem  12867  isprm6  12873  pw2dvdslemn  12891  pw2dvdseu  12894  sqrt2irrap  12906  pythagtriplem2  12993  pythagtrip  13010  pclemub  13014  pcqmul  13030  pcexp  13036  pcneg  13052  pcprmpw2  13060  pcadd  13067  pcmpt  13070  4sqlem13m  13130  ballotfilemcdc  13171  ballotfilemfc0  13180  ballotfilemfcc  13181  ennnfonelemrnh  13255  ennnfonelemnn0  13261  ctinfomlemom  13266  ctiunctlemfo  13278  nninfdclemf1  13291  imasival  13574  gsumpropd2  13660  sgrppropd  13680  ismndd  13702  mndpropd  13705  mhmeql  13751  mhmmnd  13873  issubg4m  13950  ssnmz  13968  conjnmzb  14037  gfsumval  14106  rngpropd  14198  ringpropd  14285  aprlring  14542  islmod  14569  psrval  14944  restbasg  15163  cnrest2  15231  cnpdis  15237  lmtopcnp  15245  txcnp  15266  txlm  15274  ismet2  15349  blininf  15419  metss2lem  15492  xmettxlem  15504  xmettx  15505  metcnp3  15506  metcnpi3  15512  addcncntoplem  15556  fsumcncntop  15562  mulcncf  15603  dedekindeulemuub  15612  dedekindeu  15618  dedekindicclemuub  15621  ivthinclemlopn  15631  ivthinclemuopn  15633  ivthinclemloc  15636  ivthinc  15638  ivthdichlem  15646  limcimo  15660  limccnp2cntop  15672  plyf  15732  plyco  15754  plycj  15756  plyrecj  15758  dvply2g  15761  logbgcd1irrap  15965  perfectlem2  15998  lgsdilem  16030  lgsquad2lem2  16085  lgsquad3  16087  2sqlem5  16122  2sqlem9  16127  usgredg4  16340  usgr1vr  16373  subuhgr  16397  subumgr  16399  clwwlknonex2lem2  16563  eupth2lemsfi  16603  depindlem3  16633  qdencn  16947  apdiff  16972  qdiff  16973