Theorem simplrr 525

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  rmob  2996  disjiun  3919  isotr  5710  riota5f  5747  tfrexlem  6224  tfrcl  6254  nnsucuniel  6384  fopwdom  6723  dif1enen  6767  fisbth  6770  fin0  6772  fin0or  6773  diffisn  6780  finexdc  6789  fientri3  6796  unfidisj  6803  undifdc  6805  ssfirab  6815  fnfi  6818  iunfidisj  6827  ordiso2  6913  difinfinf  6979  ctmlemr  6986  exmidfodomrlemr  7051  addcmpblnq  7168  mulcmpblnq  7169  ordpipqqs  7175  ltexnqq  7209  addcmpblnq0  7244  mulcmpblnq0  7245  prmu  7279  addlocpr  7337  prmuloc  7367  prmuloc2  7368  ltaddpr  7398  ltexprlemopl  7402  ltexprlemopu  7404  ltexprlemloc  7408  ltexprlemrl  7411  ltexprlemru  7413  addcanprleml  7415  addcanprlemu  7416  aptiprleml  7440  aptiprlemu  7441  ltmprr  7443  cauappcvgprlemloc  7453  archrecpr  7465  caucvgprlemloc  7476  caucvgprprlemloc  7504  caucvgprprlemexbt  7507  suplocexprlemdisj  7521  suplocexprlemloc  7522  addcmpblnr  7540  mulcmpblnrlemg  7541  mulcmpblnr  7542  ltsrprg  7548  mulgt0sr  7579  caucvgsrlemgt1  7596  suplocsrlemb  7607  axmulcl  7667  axarch  7692  axcaucvglemres  7700  axpre-suploclemres  7702  axpre-suploc  7703  readdcan  7895  cnegexlem1  7930  negeu  7946  add20  8229  apreap  8342  cru  8357  apsym  8361  apcotr  8362  apadd1  8363  apneg  8366  mulext1  8367  divdivdivap  8466  ltmul12a  8611  lemul12a  8613  lt2mul2div  8630  ledivdiv  8641  lediv12a  8645  qapne  9424  xleadd1a  9649  ixxss12  9682  ioodisj  9769  fz0fzelfz0  9897  qtri3or  10013  exbtwnzlemstep  10018  exbtwnzlemex  10020  exbtwnz  10021  rebtwn2zlemstep  10023  rebtwn2z  10025  qbtwnre  10027  btwnzge0  10066  iseqf1olemqf1o  10259  mulexpzap  10326  leexp1a  10341  expnbnd  10408  hashen  10523  fihashdom  10542  hashun  10544  zfz1iso  10577  cjap  10671  cvg1nlemres  10750  rsqrmo  10792  abs3lem  10876  cau3lem  10879  rexanre  10985  xrmaxltsup  11020  climcau  11109  sumeq2  11121  summodc  11145  fsum3cvg3  11158  fsum2d  11197  prodeq2  11319  eirrap  11473  addmodlteqALT  11546  divalglemeunn  11607  divalglemeuneg  11609  zsupcllemstep  11627  bezoutlemnewy  11673  bezoutlemstep  11674  bezoutlemmain  11675  bezoutlembi  11682  bezoutlemeu  11684  rpdvds  11769  isprm6  11814  pw2dvdslemn  11832  pw2dvdseu  11835  sqrt2irrap  11847  ennnfonelemrnh  11918  ennnfonelemnn0  11924  ctinfomlemom  11929  ctiunctlemfo  11941  restbasg  12326  cnrest2  12394  cnpdis  12400  lmtopcnp  12408  txcnp  12429  txlm  12437  ismet2  12512  blininf  12582  metss2lem  12655  xmettxlem  12667  xmettx  12668  metcnp3  12669  metcnpi3  12675  addcncntoplem  12709  fsumcncntop  12714  mulcncf  12749  dedekindeulemuub  12753  dedekindeu  12759  dedekindicclemuub  12762  ivthinclemlopn  12772  ivthinclemuopn  12774  ivthinclemloc  12777  ivthinc  12779  limcimo  12792  limccnp2cntop  12804  qdencn  13211