Theorem simplrl 537

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simplrl	|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )

Proof of Theorem simplrl

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	ad2antlr 489	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )

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  3126  disjiun  4088  f1imass  5925  riota5f  6008  tfrexlem  6543  tfrcl  6573  nnsucuniel  6706  nntr2  6714  pw2f1odclem  7063  fopwdom  7065  fidceq  7099  fisbth  7115  fidcen  7131  fientri3  7150  unsnfidcex  7155  undifdc  7159  iunfidisj  7188  fiuni  7220  ordiso2  7277  nninfninc  7365  acfun  7465  2omotaplemap  7519  ccfunen  7526  addcmpblnq  7630  mulcmpblnq  7631  ordpipqqs  7637  addcmpblnq0  7706  mulcmpblnq0  7707  prml  7740  addlocpr  7799  prmuloc  7829  mullocpr  7834  ltexprlemopl  7864  ltexprlemopu  7866  ltexprlemloc  7870  ltexprlemrl  7873  ltexprlemru  7875  addcanprleml  7877  addcanprlemu  7878  aptiprleml  7902  ltmprr  7905  cauappcvgprlemopl  7909  cauappcvgprlemopu  7911  cauappcvgprlemloc  7915  caucvgprlemopl  7932  caucvgprlemopu  7934  caucvgprlemloc  7938  caucvgprprlemopu  7962  caucvgprprlemloc  7966  caucvgprprlemexbt  7969  caucvgprprlemaddq  7971  suplocexprlemrl  7980  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemub  7986  addcmpblnr  8002  mulcmpblnrlemg  8003  mulcmpblnr  8004  ltsrprg  8010  mulgt0sr  8041  caucvgsrlemgt1  8058  suplocsrlemb  8069  axmulcl  8129  axcaucvglemres  8162  axpre-suploclemres  8164  axpre-suploc  8165  cnegexlem1  8396  negeu  8412  add20  8696  apreap  8809  cru  8824  apsym  8828  apcotr  8829  apadd1  8830  apneg  8833  mulext1  8834  mulge0  8841  mulap0  8876  divdivdivap  8935  prodgt0  9074  ltmul12a  9082  lt2mul2div  9101  ledivdiv  9112  lediv12a  9116  qapne  9917  xleadd1a  10152  ixxss12  10185  elfz0ubfz0  10405  qtri3or  10546  exbtwnzlemstep  10553  exbtwnzlemex  10555  exbtwnz  10556  rebtwn2zlemstep  10558  rebtwn2z  10560  btwnzge0  10606  iseqf1olemqf1o  10814  mulexpzap  10887  leexp1a  10902  hashen  11092  fihashdom  11112  hashun  11114  swrdccatin1  11355  pfxccatin12lem3  11362  pfxccat3  11364  cjap  11529  cvg1nlemres  11608  rsqrmo  11650  abslt  11711  abs3lem  11734  cau3lem  11737  rexanre  11843  xrmaxltsup  11881  climcau  11970  sumeq2  11982  summodc  12007  fisumss  12016  fsum2d  12059  fsumabs  12089  fsumiun  12101  prodeq2  12181  prodmodclem2  12201  fprodcl2lem  12229  fprodap0  12245  fprod2d  12247  fprodrec  12253  fprodap0f  12260  fprodle  12264  eirrap  12402  divalglemeunn  12545  divalglemeuneg  12547  bezoutlemnewy  12630  bezoutlemstep  12631  bezoutlemmain  12632  bezoutlembi  12639  bezoutlemeu  12641  qredeu  12732  isprm5lem  12776  pw2dvdseu  12803  sqrt2irrap  12815  pythagtriplem2  12902  pythagtrip  12919  pclemub  12923  pcqmul  12939  pcexp  12945  pcneg  12961  pcprmpw2  12969  pcadd  12976  prmpwdvds  12991  4sqlem13m  13039  ennnfonelemg  13087  ennnfonelemrnh  13100  ctiunctlemfo  13123  nninfdclemf1  13136  imasival  13452  sgrppropd  13559  ismndd  13583  mndpropd  13586  mhmeql  13638  mhmmnd  13766  mulgfng  13774  issubg4m  13843  ssnmz  13861  conjnmzb  13930  rngpropd  14032  ringpropd  14115  dvdsrtr  14179  islmod  14370  mplsubgfilemcl  14783  restbasg  14962  cnpnei  15013  cnptoprest2  15034  cnpdis  15036  lmtopcnp  15044  txcnp  15065  ismet2  15148  blininf  15218  metss2lem  15291  xmettxlem  15303  xmettx  15304  metcnp  15306  metcnpi3  15311  addcncntoplem  15355  fsumcncntop  15361  mulc1cncf  15383  cncfco  15385  mulcncf  15402  dedekindeulemuub  15411  dedekindeu  15417  dedekindicclemuub  15420  ivthinclemloc  15435  ivthinc  15437  limcimo  15459  limccnp2cntop  15471  dveflem  15520  plyf  15531  plyco  15553  plycj  15555  dvply2g  15560  logbgcd1irrap  15764  perfectlem2  15797  lgsdilem  15829  lgsquad2lem2  15884  lgsquad3  15886  2sqlem5  15921  2sqlem9  15926  usgredg4  16139  usgr1eop  16169  usgr1vr  16172  subuhgr  16196  subumgr  16198  subusgr  16199  clwwlknonex2lem2  16362  2omap  16698  pw1map  16700  qdencn  16738  apdiff  16763  qdiff  16764  gfsumval  16792