Theorem simplrr 538

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  3139  disjiun  4109  isotr  5995  riota5f  6038  tfrexlem  6578  tfrcl  6608  nnsucuniel  6741  pw2f1odclem  7100  fopwdom  7102  dif1enen  7150  fisbth  7153  fin0  7155  fin0or  7156  diffisn  7163  fidcen  7169  finexdc  7173  elssdc  7175  fientri3  7188  unfidisj  7195  undifdc  7197  ssfirab  7210  fnfi  7216  iunfidisj  7226  mapfi  7227  fissfi  7229  dcfi  7281  2omap  7282  ordiso2  7339  difinfinf  7405  ctmlemr  7412  exmidfodomrlemr  7518  2omotaplemap  7587  cc2lem  7596  cc3  7598  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  ltexnqq  7739  addcmpblnq0  7774  mulcmpblnq0  7775  prmu  7809  addlocpr  7867  prmuloc  7897  prmuloc2  7898  ltaddpr  7928  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemloc  7938  ltexprlemrl  7941  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  aptiprleml  7970  aptiprlemu  7971  ltmprr  7973  cauappcvgprlemloc  7983  archrecpr  7995  caucvgprlemloc  8006  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  suplocexprlemdisj  8051  suplocexprlemloc  8052  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  ltsrprg  8078  mulgt0sr  8109  caucvgsrlemgt1  8126  suplocsrlemb  8137  axmulcl  8197  axarch  8222  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  readdcan  8429  cnegexlem1  8464  negeu  8480  add20  8765  apreap  8878  cru  8893  apsym  8897  apcotr  8898  apadd1  8899  apneg  8902  mulext1  8903  divdivdivap  9004  ltmul12a  9151  lemul12a  9153  lt2mul2div  9170  ledivdiv  9181  lediv12a  9185  qapne  9989  xleadd1a  10225  ixxss12  10258  ioodisj  10345  fz0fzelfz0  10483  zsupcllemstep  10611  zsupssdc  10622  qtri3or  10624  exbtwnzlemstep  10631  exbtwnzlemex  10633  exbtwnz  10634  rebtwn2zlemstep  10636  rebtwn2z  10638  qbtwnre  10640  btwnzge0  10684  iseqf1olemqf1o  10892  mulexpzap  10965  leexp1a  10980  expnbnd  11050  hashen  11172  fihashdom  11192  hashun  11194  zfz1iso  11238  swrdccat  11452  reuccatpfxs1  11464  cjap  11616  cvg1nlemres  11695  rsqrmo  11737  abs3lem  11821  cau3lem  11824  rexanre  11930  xrmaxltsup  11968  climcau  12057  sumeq2  12069  summodc  12094  fsum3cvg3  12107  fsum2d  12146  prodeq2  12268  prodmodclem2  12288  fprod2d  12334  eirrap  12489  addmodlteqALT  12570  divalglemeunn  12632  divalglemeuneg  12634  bezoutlemnewy  12717  bezoutlemstep  12718  bezoutlemmain  12719  bezoutlembi  12726  bezoutlemeu  12728  rpdvds  12821  isprm5lem  12863  isprm6  12869  pw2dvdslemn  12887  pw2dvdseu  12890  sqrt2irrap  12902  pythagtriplem2  12989  pythagtrip  13006  pclemub  13010  pcqmul  13026  pcexp  13032  pcneg  13048  pcprmpw2  13056  pcadd  13063  pcmpt  13066  4sqlem13m  13126  ballotfilemcdc  13167  ballotfilemfc0  13176  ballotfilemfcc  13177  ennnfonelemrnh  13251  ennnfonelemnn0  13257  ctinfomlemom  13262  ctiunctlemfo  13274  nninfdclemf1  13287  imasival  13603  gsumpropd2  13690  sgrppropd  13710  ismndd  13734  mndpropd  13737  mhmeql  13789  mhmmnd  13917  issubg4m  13994  ssnmz  14012  conjnmzb  14081  rngpropd  14183  ringpropd  14266  aprlring  14523  islmod  14551  psrval  14926  restbasg  15145  cnrest2  15213  cnpdis  15219  lmtopcnp  15227  txcnp  15248  txlm  15256  ismet2  15331  blininf  15401  metss2lem  15474  xmettxlem  15486  xmettx  15487  metcnp3  15488  metcnpi3  15494  addcncntoplem  15538  fsumcncntop  15544  mulcncf  15585  dedekindeulemuub  15594  dedekindeu  15600  dedekindicclemuub  15603  ivthinclemlopn  15613  ivthinclemuopn  15615  ivthinclemloc  15618  ivthinc  15620  ivthdichlem  15628  limcimo  15642  limccnp2cntop  15654  plyf  15714  plyco  15736  plycj  15738  plyrecj  15740  dvply2g  15743  logbgcd1irrap  15947  perfectlem2  15980  lgsdilem  16012  lgsquad2lem2  16067  lgsquad3  16069  2sqlem5  16104  2sqlem9  16109  usgredg4  16322  usgr1vr  16355  subuhgr  16379  subumgr  16381  clwwlknonex2lem2  16545  eupth2lemsfi  16585  depindlem3  16615  qdencn  16919  apdiff  16944  qdiff  16945  trimul0or  16957  gfsumval  16974