Theorem simplrl 535

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  3122  disjiun  4078  f1imass  5904  riota5f  5987  tfrexlem  6486  tfrcl  6516  nnsucuniel  6649  nntr2  6657  pw2f1odclem  7003  fopwdom  7005  fidceq  7039  fisbth  7053  fidcen  7069  fientri3  7088  unsnfidcex  7093  undifdc  7097  iunfidisj  7124  fiuni  7156  ordiso2  7213  nninfninc  7301  acfun  7400  2omotaplemap  7454  ccfunen  7461  addcmpblnq  7565  mulcmpblnq  7566  ordpipqqs  7572  addcmpblnq0  7641  mulcmpblnq0  7642  prml  7675  addlocpr  7734  prmuloc  7764  mullocpr  7769  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemloc  7805  ltexprlemrl  7808  ltexprlemru  7810  addcanprleml  7812  addcanprlemu  7813  aptiprleml  7837  ltmprr  7840  cauappcvgprlemopl  7844  cauappcvgprlemopu  7846  cauappcvgprlemloc  7850  caucvgprlemopl  7867  caucvgprlemopu  7869  caucvgprlemloc  7873  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlemexbt  7904  caucvgprprlemaddq  7906  suplocexprlemrl  7915  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemub  7921  addcmpblnr  7937  mulcmpblnrlemg  7938  mulcmpblnr  7939  ltsrprg  7945  mulgt0sr  7976  caucvgsrlemgt1  7993  suplocsrlemb  8004  axmulcl  8064  axcaucvglemres  8097  axpre-suploclemres  8099  axpre-suploc  8100  cnegexlem1  8332  negeu  8348  add20  8632  apreap  8745  cru  8760  apsym  8764  apcotr  8765  apadd1  8766  apneg  8769  mulext1  8770  mulge0  8777  mulap0  8812  divdivdivap  8871  prodgt0  9010  ltmul12a  9018  lt2mul2div  9037  ledivdiv  9048  lediv12a  9052  qapne  9846  xleadd1a  10081  ixxss12  10114  elfz0ubfz0  10333  qtri3or  10472  exbtwnzlemstep  10479  exbtwnzlemex  10481  exbtwnz  10482  rebtwn2zlemstep  10484  rebtwn2z  10486  btwnzge0  10532  iseqf1olemqf1o  10740  mulexpzap  10813  leexp1a  10828  hashen  11018  fihashdom  11037  hashun  11039  swrdccatin1  11272  pfxccatin12lem3  11279  pfxccat3  11281  cjap  11432  cvg1nlemres  11511  rsqrmo  11553  abslt  11614  abs3lem  11637  cau3lem  11640  rexanre  11746  xrmaxltsup  11784  climcau  11873  sumeq2  11885  summodc  11909  fisumss  11918  fsum2d  11961  fsumabs  11991  fsumiun  12003  prodeq2  12083  prodmodclem2  12103  fprodcl2lem  12131  fprodap0  12147  fprod2d  12149  fprodrec  12155  fprodap0f  12162  fprodle  12166  eirrap  12304  divalglemeunn  12447  divalglemeuneg  12449  bezoutlemnewy  12532  bezoutlemstep  12533  bezoutlemmain  12534  bezoutlembi  12541  bezoutlemeu  12543  qredeu  12634  isprm5lem  12678  pw2dvdseu  12705  sqrt2irrap  12717  pythagtriplem2  12804  pythagtrip  12821  pclemub  12825  pcqmul  12841  pcexp  12847  pcneg  12863  pcprmpw2  12871  pcadd  12878  prmpwdvds  12893  4sqlem13m  12941  ennnfonelemg  12989  ennnfonelemrnh  13002  ctiunctlemfo  13025  nninfdclemf1  13038  imasival  13354  sgrppropd  13461  ismndd  13485  mndpropd  13488  mhmeql  13540  mhmmnd  13668  mulgfng  13676  issubg4m  13745  ssnmz  13763  conjnmzb  13832  rngpropd  13933  ringpropd  14016  dvdsrtr  14080  islmod  14270  mplsubgfilemcl  14678  restbasg  14857  cnpnei  14908  cnptoprest2  14929  cnpdis  14931  lmtopcnp  14939  txcnp  14960  ismet2  15043  blininf  15113  metss2lem  15186  xmettxlem  15198  xmettx  15199  metcnp  15201  metcnpi3  15206  addcncntoplem  15250  fsumcncntop  15256  mulc1cncf  15278  cncfco  15280  mulcncf  15297  dedekindeulemuub  15306  dedekindeu  15312  dedekindicclemuub  15315  ivthinclemloc  15330  ivthinc  15332  limcimo  15354  limccnp2cntop  15366  dveflem  15415  plyf  15426  plyco  15448  plycj  15450  dvply2g  15455  logbgcd1irrap  15659  perfectlem2  15689  lgsdilem  15721  lgsquad2lem2  15776  lgsquad3  15778  2sqlem5  15813  2sqlem9  15818  usgredg4  16028  2omap  16418  pw1map  16420  qdencn  16455  apdiff  16476