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  3078  disjiun  4024  isotr  5859  riota5f  5898  tfrexlem  6387  tfrcl  6417  nnsucuniel  6548  pw2f1odclem  6890  fopwdom  6892  dif1enen  6936  fisbth  6939  fin0  6941  fin0or  6942  diffisn  6949  finexdc  6958  fientri3  6971  unfidisj  6978  undifdc  6980  ssfirab  6990  fnfi  6995  iunfidisj  7005  dcfi  7040  ordiso2  7094  difinfinf  7160  ctmlemr  7167  exmidfodomrlemr  7262  2omotaplemap  7317  cc2lem  7326  cc3  7328  addcmpblnq  7427  mulcmpblnq  7428  ordpipqqs  7434  ltexnqq  7468  addcmpblnq0  7503  mulcmpblnq0  7504  prmu  7538  addlocpr  7596  prmuloc  7626  prmuloc2  7627  ltaddpr  7657  ltexprlemopl  7661  ltexprlemopu  7663  ltexprlemloc  7667  ltexprlemrl  7670  ltexprlemru  7672  addcanprleml  7674  addcanprlemu  7675  aptiprleml  7699  aptiprlemu  7700  ltmprr  7702  cauappcvgprlemloc  7712  archrecpr  7724  caucvgprlemloc  7735  caucvgprprlemloc  7763  caucvgprprlemexbt  7766  suplocexprlemdisj  7780  suplocexprlemloc  7781  addcmpblnr  7799  mulcmpblnrlemg  7800  mulcmpblnr  7801  ltsrprg  7807  mulgt0sr  7838  caucvgsrlemgt1  7855  suplocsrlemb  7866  axmulcl  7926  axarch  7951  axcaucvglemres  7959  axpre-suploclemres  7961  axpre-suploc  7962  readdcan  8159  cnegexlem1  8194  negeu  8210  add20  8493  apreap  8606  cru  8621  apsym  8625  apcotr  8626  apadd1  8627  apneg  8630  mulext1  8631  divdivdivap  8732  ltmul12a  8879  lemul12a  8881  lt2mul2div  8898  ledivdiv  8909  lediv12a  8913  qapne  9704  xleadd1a  9939  ixxss12  9972  ioodisj  10059  fz0fzelfz0  10193  qtri3or  10310  exbtwnzlemstep  10316  exbtwnzlemex  10318  exbtwnz  10319  rebtwn2zlemstep  10321  rebtwn2z  10323  qbtwnre  10325  btwnzge0  10369  iseqf1olemqf1o  10577  mulexpzap  10650  leexp1a  10665  expnbnd  10734  hashen  10855  fihashdom  10874  hashun  10876  zfz1iso  10912  cjap  11050  cvg1nlemres  11129  rsqrmo  11171  abs3lem  11255  cau3lem  11258  rexanre  11364  xrmaxltsup  11401  climcau  11490  sumeq2  11502  summodc  11526  fsum3cvg3  11539  fsum2d  11578  prodeq2  11700  prodmodclem2  11720  fprod2d  11766  eirrap  11921  addmodlteqALT  12001  divalglemeunn  12062  divalglemeuneg  12064  zsupcllemstep  12082  zsupssdc  12091  bezoutlemnewy  12133  bezoutlemstep  12134  bezoutlemmain  12135  bezoutlembi  12142  bezoutlemeu  12144  rpdvds  12237  isprm5lem  12279  isprm6  12285  pw2dvdslemn  12303  pw2dvdseu  12306  sqrt2irrap  12318  pythagtriplem2  12404  pythagtrip  12421  pclemub  12425  pcqmul  12441  pcexp  12447  pcneg  12463  pcprmpw2  12471  pcadd  12478  pcmpt  12481  4sqlem13m  12541  ennnfonelemrnh  12573  ennnfonelemnn0  12579  ctinfomlemom  12584  ctiunctlemfo  12596  nninfdclemf1  12609  imasival  12889  gsumpropd2  12976  sgrppropd  12996  ismndd  13018  mndpropd  13021  mhmeql  13064  mhmmnd  13186  issubg4m  13263  ssnmz  13281  conjnmzb  13350  rngpropd  13451  ringpropd  13534  islmod  13787  psrval  14152  restbasg  14336  cnrest2  14404  cnpdis  14410  lmtopcnp  14418  txcnp  14439  txlm  14447  ismet2  14522  blininf  14592  metss2lem  14665  xmettxlem  14677  xmettx  14678  metcnp3  14679  metcnpi3  14685  addcncntoplem  14719  fsumcncntop  14724  mulcncf  14762  dedekindeulemuub  14771  dedekindeu  14777  dedekindicclemuub  14780  ivthinclemlopn  14790  ivthinclemuopn  14792  ivthinclemloc  14795  ivthinc  14797  ivthdichlem  14805  limcimo  14819  limccnp2cntop  14831  plyf  14883  logbgcd1irrap  15102  lgsdilem  15143  2sqlem5  15206  2sqlem9  15211  qdencn  15517  apdiff  15538