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  2931  disjiun  3840  isotr  5595  riota5f  5632  tfrexlem  6099  tfrcl  6129  nnsucuniel  6256  fopwdom  6550  dif1enen  6594  fisbth  6597  fin0  6599  fin0or  6600  diffisn  6607  finexdc  6616  fientri3  6623  unfidisj  6630  undifdc  6632  ssfirab  6641  fnfi  6644  iunfidisj  6653  ordiso2  6726  exmidfodomrlemr  6826  addcmpblnq  6924  mulcmpblnq  6925  ordpipqqs  6931  ltexnqq  6965  addcmpblnq0  7000  mulcmpblnq0  7001  prmu  7035  addlocpr  7093  prmuloc  7123  prmuloc2  7124  ltaddpr  7154  ltexprlemopl  7158  ltexprlemopu  7160  ltexprlemloc  7164  ltexprlemrl  7167  ltexprlemru  7169  addcanprleml  7171  addcanprlemu  7172  aptiprleml  7196  aptiprlemu  7197  ltmprr  7199  cauappcvgprlemloc  7209  archrecpr  7221  caucvgprlemloc  7232  caucvgprprlemloc  7260  caucvgprprlemexbt  7263  addcmpblnr  7283  mulcmpblnrlemg  7284  mulcmpblnr  7285  ltsrprg  7291  mulgt0sr  7321  caucvgsrlemgt1  7338  axmulcl  7401  axarch  7424  axcaucvglemres  7432  readdcan  7620  cnegexlem1  7655  negeu  7671  add20  7950  apreap  8062  cru  8077  apsym  8081  apcotr  8082  apadd1  8083  apneg  8086  mulext1  8087  divdivdivap  8178  ltmul12a  8319  lemul12a  8321  lt2mul2div  8338  ledivdiv  8349  lediv12a  8353  qapne  9122  ixxss12  9322  ioodisj  9408  fz0fzelfz0  9534  qtri3or  9650  exbtwnzlemstep  9655  exbtwnzlemex  9657  exbtwnz  9658  rebtwn2zlemstep  9660  rebtwn2z  9662  qbtwnre  9664  btwnzge0  9703  iseqf1olemqf1o  9918  mulexpzap  9991  leexp1a  10006  expnbnd  10073  hashen  10188  fihashdom  10207  hashun  10209  zfz1iso  10242  cjap  10336  cvg1nlemres  10414  rsqrmo  10456  abs3lem  10540  cau3lem  10543  rexanre  10649  climcau  10732  sumeq2  10744  isummo  10769  fsum3cvg3  10785  fsum2d  10825  eirrap  11061  addmodlteqALT  11134  divalglemeunn  11195  divalglemeuneg  11197  zsupcllemstep  11215  bezoutlemnewy  11259  bezoutlemstep  11260  bezoutlemmain  11261  bezoutlembi  11268  bezoutlemeu  11270  rpdvds  11355  isprm6  11400  pw2dvdslemn  11417  pw2dvdseu  11420  sqrt2irrap  11432  qdencn  11870