Theorem simplrr 542

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 493	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  rmob  3145  disjiun  4125  isotr  6025  riota5f  6068  tfrexlem  6610  tfrcl  6640  nnsucuniel  6773  pw2f1odclem  7140  fopwdom  7142  dif1enen  7190  fisbth  7193  fin0  7195  fin0or  7196  diffisn  7203  fidcen  7209  finexdc  7213  elssdc  7215  fientri3  7228  unfidisj  7235  undifdc  7237  ssfirab  7250  fnfi  7256  iunfidisj  7266  mapfi  7267  fissfi  7269  dcfi  7321  2omap  7325  ordiso2  7382  difinfinf  7448  ctmlemr  7455  exmidfodomrlemr  7561  2omotaplemap  7630  cc2lem  7639  cc3  7641  addcmpblnq  7741  mulcmpblnq  7742  ordpipqqs  7748  ltexnqq  7782  addcmpblnq0  7817  mulcmpblnq0  7818  prmu  7852  addlocpr  7910  prmuloc  7940  prmuloc2  7941  ltaddpr  7971  ltexprlemopl  7975  ltexprlemopu  7977  ltexprlemloc  7981  ltexprlemrl  7984  ltexprlemru  7986  addcanprleml  7988  addcanprlemu  7989  aptiprleml  8013  aptiprlemu  8014  ltmprr  8016  cauappcvgprlemloc  8026  archrecpr  8038  caucvgprlemloc  8049  caucvgprprlemloc  8077  caucvgprprlemexbt  8080  suplocexprlemdisj  8094  suplocexprlemloc  8095  addcmpblnr  8113  mulcmpblnrlemg  8114  mulcmpblnr  8115  ltsrprg  8121  mulgt0sr  8152  caucvgsrlemgt1  8169  suplocsrlemb  8180  axmulcl  8240  axarch  8265  axcaucvglemres  8273  axpre-suploclemres  8275  axpre-suploc  8276  readdcan  8474  cnegexlem1  8509  negeu  8525  add20  8810  apreap  8924  cru  8939  apsym  8943  apcotr  8944  apadd1  8945  apneg  8948  mulext1  8949  divdivdivap  9052  ltmul12a  9199  lemul12a  9201  lt2mul2div  9218  ledivdiv  9229  lediv12a  9233  qapne  10055  xleadd1a  10292  ixxss12  10325  ioodisj  10412  fz0fzelfz0  10551  zsupcllemstep  10679  zsupssdc  10690  qtri3or  10692  exbtwnzlemstep  10699  exbtwnzlemex  10701  exbtwnz  10702  rebtwn2zlemstep  10704  rebtwn2z  10706  qbtwnre  10708  btwnzge0  10756  iseqf1olemqf1o  10964  mulexpzap  11037  leexp1a  11052  expnbnd  11122  hashen  11245  fihashdom  11265  hashun  11267  hashf1  11309  zfz1iso  11315  swrdccat  11529  reuccatpfxs1  11541  cjap  11694  cvg1nlemres  11773  rsqrmo  11815  abs3lem  11900  cau3lem  11903  rexanre  12009  fiidxsupcl  12018  xrmaxltsup  12049  climcau  12138  sumeq2  12150  summodc  12175  fsum3cvg3  12188  fsum2d  12227  prodeq2  12349  prodmodclem2  12369  fprod2d  12415  eirrap  12570  addmodlteqALT  12651  divalglemeunn  12713  divalglemeuneg  12715  bezoutlemnewy  12798  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlembi  12807  bezoutlemeu  12809  rpdvds  12902  isprm5lem  12945  isprm6  12951  pwbdvdslemn  12969  pwbdvdseu  12972  sqrt2irrap  12985  pythagtriplem2  13074  pythagtrip  13091  pclemub  13095  pcqmul  13111  pcexp  13117  pcneg  13133  pcprmpw2  13141  pcadd  13148  pcmpt  13151  4sqlem13m  13211  ballotfilemcdc  13281  ballotfilemfc0  13290  ballotfilemfcc  13291  ennnfonelemrnh  13365  ennnfonelemnn0  13371  ctinfomlemom  13376  ctiunctlemfo  13388  nninfdclemf1  13401  imasival  13686  sgrppropd  13787  ismndd  13809  mndpropd  13812  mhmeql  13858  mhmmnd  13978  issubg4m  14055  ssnmz  14073  conjnmzb  14142  gsumvalfi  14242  rngpropd  14361  ringpropd  14450  aprlring  14709  islmod  14736  assapropd  15123  psrval  15161  psrbaglefifi  15175  psrbaglefimap  15183  psrbagmax  15190  mplsubrglemcl  15249  restbasg  15427  cnrest2  15495  cnpdis  15501  lmtopcnp  15509  txcnp  15530  txlm  15538  ismet2  15613  blininf  15683  metss2lem  15756  xmettxlem  15768  xmettx  15769  metcnp3  15770  metcnpi3  15776  addcncntoplem  15820  fsumcncntop  15826  mulcncf  15867  dedekindeulemuub  15876  dedekindeu  15882  dedekindicclemuub  15885  ivthinclemlopn  15895  ivthinclemuopn  15897  ivthinclemloc  15900  ivthinc  15902  ivthdichlem  15910  limcimo  15924  limccnp2cntop  15936  plyf  15996  plyco  16018  plycj  16020  plyrecj  16022  dvply2g  16025  logdivlt  16157  logbgcd1irrap  16239  zprmlogbap  16251  perfectlem2  16333  lgsdilem  16384  lgsquad2lem2  16439  lgsquad3  16441  2sqlem5  16476  2sqlem9  16481  usgredg4  16694  usgr1vr  16727  subuhgr  16751  subumgr  16753  clwwlknonex2lem2  16917  eupth2lemsfi  16957  depindlem3  16987  qdencn  17311  apdiff  17337  qdiff  17338