Theorem simplrr 536

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  3070  disjiun  4013  isotr  5838  riota5f  5876  tfrexlem  6359  tfrcl  6389  nnsucuniel  6520  pw2f1odclem  6862  fopwdom  6864  dif1enen  6908  fisbth  6911  fin0  6913  fin0or  6914  diffisn  6921  finexdc  6930  fientri3  6943  unfidisj  6950  undifdc  6952  ssfirab  6962  fnfi  6966  iunfidisj  6975  dcfi  7010  ordiso2  7064  difinfinf  7130  ctmlemr  7137  exmidfodomrlemr  7231  2omotaplemap  7286  cc2lem  7295  cc3  7297  addcmpblnq  7396  mulcmpblnq  7397  ordpipqqs  7403  ltexnqq  7437  addcmpblnq0  7472  mulcmpblnq0  7473  prmu  7507  addlocpr  7565  prmuloc  7595  prmuloc2  7596  ltaddpr  7626  ltexprlemopl  7630  ltexprlemopu  7632  ltexprlemloc  7636  ltexprlemrl  7639  ltexprlemru  7641  addcanprleml  7643  addcanprlemu  7644  aptiprleml  7668  aptiprlemu  7669  ltmprr  7671  cauappcvgprlemloc  7681  archrecpr  7693  caucvgprlemloc  7704  caucvgprprlemloc  7732  caucvgprprlemexbt  7735  suplocexprlemdisj  7749  suplocexprlemloc  7750  addcmpblnr  7768  mulcmpblnrlemg  7769  mulcmpblnr  7770  ltsrprg  7776  mulgt0sr  7807  caucvgsrlemgt1  7824  suplocsrlemb  7835  axmulcl  7895  axarch  7920  axcaucvglemres  7928  axpre-suploclemres  7930  axpre-suploc  7931  readdcan  8127  cnegexlem1  8162  negeu  8178  add20  8461  apreap  8574  cru  8589  apsym  8593  apcotr  8594  apadd1  8595  apneg  8598  mulext1  8599  divdivdivap  8700  ltmul12a  8847  lemul12a  8849  lt2mul2div  8866  ledivdiv  8877  lediv12a  8881  qapne  9669  xleadd1a  9903  ixxss12  9936  ioodisj  10023  fz0fzelfz0  10157  qtri3or  10273  exbtwnzlemstep  10278  exbtwnzlemex  10280  exbtwnz  10281  rebtwn2zlemstep  10283  rebtwn2z  10285  qbtwnre  10287  btwnzge0  10331  iseqf1olemqf1o  10524  mulexpzap  10591  leexp1a  10606  expnbnd  10675  hashen  10796  fihashdom  10815  hashun  10817  zfz1iso  10853  cjap  10947  cvg1nlemres  11026  rsqrmo  11068  abs3lem  11152  cau3lem  11155  rexanre  11261  xrmaxltsup  11298  climcau  11387  sumeq2  11399  summodc  11423  fsum3cvg3  11436  fsum2d  11475  prodeq2  11597  prodmodclem2  11617  fprod2d  11663  eirrap  11817  addmodlteqALT  11897  divalglemeunn  11958  divalglemeuneg  11960  zsupcllemstep  11978  zsupssdc  11987  bezoutlemnewy  12029  bezoutlemstep  12030  bezoutlemmain  12031  bezoutlembi  12038  bezoutlemeu  12040  rpdvds  12131  isprm5lem  12173  isprm6  12179  pw2dvdslemn  12197  pw2dvdseu  12200  sqrt2irrap  12212  pythagtriplem2  12298  pythagtrip  12315  pclemub  12319  pcqmul  12335  pcexp  12341  pcneg  12357  pcprmpw2  12365  pcadd  12372  pcmpt  12375  4sqlem13m  12435  ennnfonelemrnh  12467  ennnfonelemnn0  12473  ctinfomlemom  12478  ctiunctlemfo  12490  nninfdclemf1  12503  imasival  12783  sgrppropd  12876  ismndd  12898  mndpropd  12901  mhmeql  12944  mhmmnd  13058  issubg4m  13132  ssnmz  13150  conjnmzb  13219  rngpropd  13309  ringpropd  13392  islmod  13607  psrval  13944  restbasg  14125  cnrest2  14193  cnpdis  14199  lmtopcnp  14207  txcnp  14228  txlm  14236  ismet2  14311  blininf  14381  metss2lem  14454  xmettxlem  14466  xmettx  14467  metcnp3  14468  metcnpi3  14474  addcncntoplem  14508  fsumcncntop  14513  mulcncf  14548  dedekindeulemuub  14552  dedekindeu  14558  dedekindicclemuub  14561  ivthinclemlopn  14571  ivthinclemuopn  14573  ivthinclemloc  14576  ivthinc  14578  limcimo  14591  limccnp2cntop  14603  logbgcd1irrap  14845  lgsdilem  14886  2sqlem5  14924  2sqlem9  14929  qdencn  15234  apdiff  15255