Theorem simplrr 526

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 481	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  3029  disjiun  3960  isotr  5761  riota5f  5798  tfrexlem  6275  tfrcl  6305  nnsucuniel  6435  fopwdom  6774  dif1enen  6818  fisbth  6821  fin0  6823  fin0or  6824  diffisn  6831  finexdc  6840  fientri3  6852  unfidisj  6859  undifdc  6861  ssfirab  6871  fnfi  6874  iunfidisj  6883  ordiso2  6969  difinfinf  7035  ctmlemr  7042  exmidfodomrlemr  7120  cc2lem  7169  cc3  7171  addcmpblnq  7270  mulcmpblnq  7271  ordpipqqs  7277  ltexnqq  7311  addcmpblnq0  7346  mulcmpblnq0  7347  prmu  7381  addlocpr  7439  prmuloc  7469  prmuloc2  7470  ltaddpr  7500  ltexprlemopl  7504  ltexprlemopu  7506  ltexprlemloc  7510  ltexprlemrl  7513  ltexprlemru  7515  addcanprleml  7517  addcanprlemu  7518  aptiprleml  7542  aptiprlemu  7543  ltmprr  7545  cauappcvgprlemloc  7555  archrecpr  7567  caucvgprlemloc  7578  caucvgprprlemloc  7606  caucvgprprlemexbt  7609  suplocexprlemdisj  7623  suplocexprlemloc  7624  addcmpblnr  7642  mulcmpblnrlemg  7643  mulcmpblnr  7644  ltsrprg  7650  mulgt0sr  7681  caucvgsrlemgt1  7698  suplocsrlemb  7709  axmulcl  7769  axarch  7794  axcaucvglemres  7802  axpre-suploclemres  7804  axpre-suploc  7805  readdcan  7998  cnegexlem1  8033  negeu  8049  add20  8332  apreap  8445  cru  8460  apsym  8464  apcotr  8465  apadd1  8466  apneg  8469  mulext1  8470  divdivdivap  8569  ltmul12a  8714  lemul12a  8716  lt2mul2div  8733  ledivdiv  8744  lediv12a  8748  qapne  9530  xleadd1a  9759  ixxss12  9792  ioodisj  9879  fz0fzelfz0  10008  qtri3or  10124  exbtwnzlemstep  10129  exbtwnzlemex  10131  exbtwnz  10132  rebtwn2zlemstep  10134  rebtwn2z  10136  qbtwnre  10138  btwnzge0  10181  iseqf1olemqf1o  10374  mulexpzap  10441  leexp1a  10456  expnbnd  10523  hashen  10640  fihashdom  10659  hashun  10661  zfz1iso  10694  cjap  10788  cvg1nlemres  10867  rsqrmo  10909  abs3lem  10993  cau3lem  10996  rexanre  11102  xrmaxltsup  11137  climcau  11226  sumeq2  11238  summodc  11262  fsum3cvg3  11275  fsum2d  11314  prodeq2  11436  prodmodclem2  11456  fprod2d  11502  eirrap  11656  addmodlteqALT  11732  divalglemeunn  11793  divalglemeuneg  11795  zsupcllemstep  11813  bezoutlemnewy  11860  bezoutlemstep  11861  bezoutlemmain  11862  bezoutlembi  11869  bezoutlemeu  11871  rpdvds  11956  isprm6  12001  pw2dvdslemn  12019  pw2dvdseu  12022  sqrt2irrap  12034  ennnfonelemrnh  12117  ennnfonelemnn0  12123  ctinfomlemom  12128  ctiunctlemfo  12140  restbasg  12528  cnrest2  12596  cnpdis  12602  lmtopcnp  12610  txcnp  12631  txlm  12639  ismet2  12714  blininf  12784  metss2lem  12857  xmettxlem  12869  xmettx  12870  metcnp3  12871  metcnpi3  12877  addcncntoplem  12911  fsumcncntop  12916  mulcncf  12951  dedekindeulemuub  12955  dedekindeu  12961  dedekindicclemuub  12964  ivthinclemlopn  12974  ivthinclemuopn  12976  ivthinclemloc  12979  ivthinc  12981  limcimo  12994  limccnp2cntop  13006  logbgcd1irrap  13247  qdencn  13561  apdiff  13582