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  3126  disjiun  4088  isotr  5967  riota5f  6008  tfrexlem  6543  tfrcl  6573  nnsucuniel  6706  pw2f1odclem  7063  fopwdom  7065  dif1enen  7112  fisbth  7115  fin0  7117  fin0or  7118  diffisn  7125  fidcen  7131  finexdc  7135  elssdc  7137  fientri3  7150  unfidisj  7157  undifdc  7159  ssfirab  7172  fnfi  7178  iunfidisj  7188  dcfi  7223  ordiso2  7277  difinfinf  7343  ctmlemr  7350  exmidfodomrlemr  7456  2omotaplemap  7519  cc2lem  7528  cc3  7530  addcmpblnq  7630  mulcmpblnq  7631  ordpipqqs  7637  ltexnqq  7671  addcmpblnq0  7706  mulcmpblnq0  7707  prmu  7741  addlocpr  7799  prmuloc  7829  prmuloc2  7830  ltaddpr  7860  ltexprlemopl  7864  ltexprlemopu  7866  ltexprlemloc  7870  ltexprlemrl  7873  ltexprlemru  7875  addcanprleml  7877  addcanprlemu  7878  aptiprleml  7902  aptiprlemu  7903  ltmprr  7905  cauappcvgprlemloc  7915  archrecpr  7927  caucvgprlemloc  7938  caucvgprprlemloc  7966  caucvgprprlemexbt  7969  suplocexprlemdisj  7983  suplocexprlemloc  7984  addcmpblnr  8002  mulcmpblnrlemg  8003  mulcmpblnr  8004  ltsrprg  8010  mulgt0sr  8041  caucvgsrlemgt1  8058  suplocsrlemb  8069  axmulcl  8129  axarch  8154  axcaucvglemres  8162  axpre-suploclemres  8164  axpre-suploc  8165  readdcan  8362  cnegexlem1  8397  negeu  8413  add20  8697  apreap  8810  cru  8825  apsym  8829  apcotr  8830  apadd1  8831  apneg  8834  mulext1  8835  divdivdivap  8936  ltmul12a  9083  lemul12a  9085  lt2mul2div  9102  ledivdiv  9113  lediv12a  9117  qapne  9916  xleadd1a  10151  ixxss12  10184  ioodisj  10271  fz0fzelfz0  10405  zsupcllemstep  10533  zsupssdc  10542  qtri3or  10544  exbtwnzlemstep  10551  exbtwnzlemex  10553  exbtwnz  10554  rebtwn2zlemstep  10556  rebtwn2z  10558  qbtwnre  10560  btwnzge0  10604  iseqf1olemqf1o  10812  mulexpzap  10885  leexp1a  10900  expnbnd  10969  hashen  11090  fihashdom  11110  hashun  11112  zfz1iso  11149  swrdccat  11363  reuccatpfxs1  11375  cjap  11527  cvg1nlemres  11606  rsqrmo  11648  abs3lem  11732  cau3lem  11735  rexanre  11841  xrmaxltsup  11879  climcau  11968  sumeq2  11980  summodc  12005  fsum3cvg3  12018  fsum2d  12057  prodeq2  12179  prodmodclem2  12199  fprod2d  12245  eirrap  12400  addmodlteqALT  12481  divalglemeunn  12543  divalglemeuneg  12545  bezoutlemnewy  12628  bezoutlemstep  12629  bezoutlemmain  12630  bezoutlembi  12637  bezoutlemeu  12639  rpdvds  12732  isprm5lem  12774  isprm6  12780  pw2dvdslemn  12798  pw2dvdseu  12801  sqrt2irrap  12813  pythagtriplem2  12900  pythagtrip  12917  pclemub  12921  pcqmul  12937  pcexp  12943  pcneg  12959  pcprmpw2  12967  pcadd  12974  pcmpt  12977  4sqlem13m  13037  ennnfonelemrnh  13098  ennnfonelemnn0  13104  ctinfomlemom  13109  ctiunctlemfo  13121  nninfdclemf1  13134  imasival  13450  gsumpropd2  13537  sgrppropd  13557  ismndd  13581  mndpropd  13584  mhmeql  13636  mhmmnd  13764  issubg4m  13841  ssnmz  13859  conjnmzb  13928  rngpropd  14030  ringpropd  14113  islmod  14367  psrval  14742  restbasg  14959  cnrest2  15027  cnpdis  15033  lmtopcnp  15041  txcnp  15062  txlm  15070  ismet2  15145  blininf  15215  metss2lem  15288  xmettxlem  15300  xmettx  15301  metcnp3  15302  metcnpi3  15308  addcncntoplem  15352  fsumcncntop  15358  mulcncf  15399  dedekindeulemuub  15408  dedekindeu  15414  dedekindicclemuub  15417  ivthinclemlopn  15427  ivthinclemuopn  15429  ivthinclemloc  15432  ivthinc  15434  ivthdichlem  15442  limcimo  15456  limccnp2cntop  15468  plyf  15528  plyco  15550  plycj  15552  plyrecj  15554  dvply2g  15557  logbgcd1irrap  15761  perfectlem2  15794  lgsdilem  15826  lgsquad2lem2  15881  lgsquad3  15883  2sqlem5  15918  2sqlem9  15923  usgredg4  16136  usgr1vr  16169  subuhgr  16193  subumgr  16195  clwwlknonex2lem2  16359  eupth2lemsfi  16399  depindlem3  16429  2omap  16695  qdencn  16735  apdiff  16760  qdiff  16761  gfsumval  16789