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  10490  zsupssdc  10499  qtri3or  10501  exbtwnzlemstep  10508  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2z  10515  qbtwnre  10517  btwnzge0  10561  iseqf1olemqf1o  10769  mulexpzap  10842  leexp1a  10857  expnbnd  10926  hashen  11047  fihashdom  11067  hashun  11069  zfz1iso  11106  swrdccat  11320  reuccatpfxs1  11332  cjap  11471  cvg1nlemres  11550  rsqrmo  11592  abs3lem  11676  cau3lem  11679  rexanre  11785  xrmaxltsup  11823  climcau  11912  sumeq2  11924  summodc  11949  fsum3cvg3  11962  fsum2d  12001  prodeq2  12123  prodmodclem2  12143  fprod2d  12189  eirrap  12344  addmodlteqALT  12425  divalglemeunn  12487  divalglemeuneg  12489  bezoutlemnewy  12572  bezoutlemstep  12573  bezoutlemmain  12574  bezoutlembi  12581  bezoutlemeu  12583  rpdvds  12676  isprm5lem  12718  isprm6  12724  pw2dvdslemn  12742  pw2dvdseu  12745  sqrt2irrap  12757  pythagtriplem2  12844  pythagtrip  12861  pclemub  12865  pcqmul  12881  pcexp  12887  pcneg  12903  pcprmpw2  12911  pcadd  12918  pcmpt  12921  4sqlem13m  12981  ennnfonelemrnh  13042  ennnfonelemnn0  13048  ctinfomlemom  13053  ctiunctlemfo  13065  nninfdclemf1  13078  imasival  13394  gsumpropd2  13481  sgrppropd  13501  ismndd  13525  mndpropd  13528  mhmeql  13580  mhmmnd  13708  issubg4m  13785  ssnmz  13803  conjnmzb  13872  rngpropd  13974  ringpropd  14057  islmod  14311  psrval  14686  restbasg  14898  cnrest2  14966  cnpdis  14972  lmtopcnp  14980  txcnp  15001  txlm  15009  ismet2  15084  blininf  15154  metss2lem  15227  xmettxlem  15239  xmettx  15240  metcnp3  15241  metcnpi3  15247  addcncntoplem  15291  fsumcncntop  15297  mulcncf  15338  dedekindeulemuub  15347  dedekindeu  15353  dedekindicclemuub  15356  ivthinclemlopn  15366  ivthinclemuopn  15368  ivthinclemloc  15371  ivthinc  15373  ivthdichlem  15381  limcimo  15395  limccnp2cntop  15407  plyf  15467  plyco  15489  plycj  15491  plyrecj  15493  dvply2g  15496  logbgcd1irrap  15700  perfectlem2  15730  lgsdilem  15762  lgsquad2lem2  15817  lgsquad3  15819  2sqlem5  15854  2sqlem9  15859  usgredg4  16072  usgr1vr  16105  subuhgr  16129  subumgr  16131  clwwlknonex2lem2  16295  eupth2lemsfi  16335  depindlem3  16353  2omap  16620  qdencn  16657  apdiff  16678  gfsumval  16706