Theorem simplrr 503

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 108	. 2 |- ( ( ps /\ ch ) -> ch )
2	1	ad2antlr 473	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  rmob  2917  isotr  5535  riota5f  5571  tfrexlem  6031  tfrcl  6061  nnsucuniel  6188  fopwdom  6482  dif1enen  6526  fisbth  6529  fin0  6531  fin0or  6532  diffisn  6539  finexdc  6545  fientri3  6552  unfidisj  6559  undifdc  6561  ssfirab  6568  fnfi  6571  ordiso2  6635  exmidfodomrlemr  6731  addcmpblnq  6829  mulcmpblnq  6830  ordpipqqs  6836  ltexnqq  6870  addcmpblnq0  6905  mulcmpblnq0  6906  prmu  6940  addlocpr  6998  prmuloc  7028  prmuloc2  7029  ltaddpr  7059  ltexprlemopl  7063  ltexprlemopu  7065  ltexprlemloc  7069  ltexprlemrl  7072  ltexprlemru  7074  addcanprleml  7076  addcanprlemu  7077  aptiprleml  7101  aptiprlemu  7102  ltmprr  7104  cauappcvgprlemloc  7114  archrecpr  7126  caucvgprlemloc  7137  caucvgprprlemloc  7165  caucvgprprlemexbt  7168  addcmpblnr  7188  mulcmpblnrlemg  7189  mulcmpblnr  7190  ltsrprg  7196  mulgt0sr  7226  caucvgsrlemgt1  7243  axmulcl  7306  axarch  7329  axcaucvglemres  7337  readdcan  7525  cnegexlem1  7560  negeu  7576  add20  7855  apreap  7964  cru  7979  apsym  7983  apcotr  7984  apadd1  7985  apneg  7988  mulext1  7989  divdivdivap  8078  ltmul12a  8215  lemul12a  8217  lt2mul2div  8234  ledivdiv  8245  lediv12a  8249  qapne  9019  ixxss12  9219  ioodisj  9305  fz0fzelfz0  9429  qtri3or  9543  exbtwnzlemstep  9548  exbtwnzlemex  9550  exbtwnz  9551  rebtwn2zlemstep  9553  rebtwn2z  9555  qbtwnre  9557  btwnzge0  9596  expivallem  9793  mulexpzap  9832  leexp1a  9847  expnbnd  9912  hashen  10027  fihashdom  10046  hashun  10048  cjap  10167  cvg1nlemres  10245  rsqrmo  10287  abs3lem  10371  cau3lem  10374  rexanre  10480  climcau  10558  sumeq2d  10570  sumeq2  10571  addmodlteqALT  10640  divalglemeunn  10701  divalglemeuneg  10703  zsupcllemstep  10721  bezoutlemnewy  10765  bezoutlemstep  10766  bezoutlemmain  10767  bezoutlembi  10774  bezoutlemeu  10776  rpdvds  10861  isprm6  10906  pw2dvdslemn  10923  pw2dvdseu  10926  sqrt2irrap  10938  qdencn  11253