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  3042  disjiun  3976  isotr  5783  riota5f  5821  tfrexlem  6298  tfrcl  6328  nnsucuniel  6459  fopwdom  6798  dif1enen  6842  fisbth  6845  fin0  6847  fin0or  6848  diffisn  6855  finexdc  6864  fientri3  6876  unfidisj  6883  undifdc  6885  ssfirab  6895  fnfi  6898  iunfidisj  6907  dcfi  6942  ordiso2  6996  difinfinf  7062  ctmlemr  7069  exmidfodomrlemr  7154  cc2lem  7203  cc3  7205  addcmpblnq  7304  mulcmpblnq  7305  ordpipqqs  7311  ltexnqq  7345  addcmpblnq0  7380  mulcmpblnq0  7381  prmu  7415  addlocpr  7473  prmuloc  7503  prmuloc2  7504  ltaddpr  7534  ltexprlemopl  7538  ltexprlemopu  7540  ltexprlemloc  7544  ltexprlemrl  7547  ltexprlemru  7549  addcanprleml  7551  addcanprlemu  7552  aptiprleml  7576  aptiprlemu  7577  ltmprr  7579  cauappcvgprlemloc  7589  archrecpr  7601  caucvgprlemloc  7612  caucvgprprlemloc  7640  caucvgprprlemexbt  7643  suplocexprlemdisj  7657  suplocexprlemloc  7658  addcmpblnr  7676  mulcmpblnrlemg  7677  mulcmpblnr  7678  ltsrprg  7684  mulgt0sr  7715  caucvgsrlemgt1  7732  suplocsrlemb  7743  axmulcl  7803  axarch  7828  axcaucvglemres  7836  axpre-suploclemres  7838  axpre-suploc  7839  readdcan  8034  cnegexlem1  8069  negeu  8085  add20  8368  apreap  8481  cru  8496  apsym  8500  apcotr  8501  apadd1  8502  apneg  8505  mulext1  8506  divdivdivap  8605  ltmul12a  8751  lemul12a  8753  lt2mul2div  8770  ledivdiv  8781  lediv12a  8785  qapne  9573  xleadd1a  9805  ixxss12  9838  ioodisj  9925  fz0fzelfz0  10058  qtri3or  10174  exbtwnzlemstep  10179  exbtwnzlemex  10181  exbtwnz  10182  rebtwn2zlemstep  10184  rebtwn2z  10186  qbtwnre  10188  btwnzge0  10231  iseqf1olemqf1o  10424  mulexpzap  10491  leexp1a  10506  expnbnd  10574  hashen  10693  fihashdom  10712  hashun  10714  zfz1iso  10750  cjap  10844  cvg1nlemres  10923  rsqrmo  10965  abs3lem  11049  cau3lem  11052  rexanre  11158  xrmaxltsup  11195  climcau  11284  sumeq2  11296  summodc  11320  fsum3cvg3  11333  fsum2d  11372  prodeq2  11494  prodmodclem2  11514  fprod2d  11560  eirrap  11714  addmodlteqALT  11793  divalglemeunn  11854  divalglemeuneg  11856  zsupcllemstep  11874  zsupssdc  11883  bezoutlemnewy  11925  bezoutlemstep  11926  bezoutlemmain  11927  bezoutlembi  11934  bezoutlemeu  11936  rpdvds  12027  isprm5lem  12069  isprm6  12075  pw2dvdslemn  12093  pw2dvdseu  12096  sqrt2irrap  12108  pythagtriplem2  12194  pythagtrip  12211  pclemub  12215  pcqmul  12231  pcexp  12237  pcneg  12252  pcprmpw2  12260  pcadd  12267  pcmpt  12269  ennnfonelemrnh  12345  ennnfonelemnn0  12351  ctinfomlemom  12356  ctiunctlemfo  12368  nninfdclemf1  12381  restbasg  12768  cnrest2  12836  cnpdis  12842  lmtopcnp  12850  txcnp  12871  txlm  12879  ismet2  12954  blininf  13024  metss2lem  13097  xmettxlem  13109  xmettx  13110  metcnp3  13111  metcnpi3  13117  addcncntoplem  13151  fsumcncntop  13156  mulcncf  13191  dedekindeulemuub  13195  dedekindeu  13201  dedekindicclemuub  13204  ivthinclemlopn  13214  ivthinclemuopn  13216  ivthinclemloc  13219  ivthinc  13221  limcimo  13234  limccnp2cntop  13246  logbgcd1irrap  13488  lgsdilem  13528  2sqlem5  13555  2sqlem9  13560  qdencn  13866  apdiff  13887