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  3125  disjiun  4083  f1imass  5915  riota5f  5998  tfrexlem  6500  tfrcl  6530  nnsucuniel  6663  nntr2  6671  pw2f1odclem  7020  fopwdom  7022  fidceq  7056  fisbth  7072  fidcen  7088  fientri3  7107  unsnfidcex  7112  undifdc  7116  iunfidisj  7145  fiuni  7177  ordiso2  7234  nninfninc  7322  acfun  7422  2omotaplemap  7476  ccfunen  7483  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  addcmpblnq0  7663  mulcmpblnq0  7664  prml  7697  addlocpr  7756  prmuloc  7786  mullocpr  7791  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  aptiprleml  7859  ltmprr  7862  cauappcvgprlemopl  7866  cauappcvgprlemopu  7868  cauappcvgprlemloc  7872  caucvgprlemopl  7889  caucvgprlemopu  7891  caucvgprlemloc  7895  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  caucvgprprlemaddq  7928  suplocexprlemrl  7937  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  ltsrprg  7967  mulgt0sr  7998  caucvgsrlemgt1  8015  suplocsrlemb  8026  axmulcl  8086  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  cnegexlem1  8354  negeu  8370  add20  8654  apreap  8767  cru  8782  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  mulge0  8799  mulap0  8834  divdivdivap  8893  prodgt0  9032  ltmul12a  9040  lt2mul2div  9059  ledivdiv  9070  lediv12a  9074  qapne  9873  xleadd1a  10108  ixxss12  10141  elfz0ubfz0  10360  qtri3or  10501  exbtwnzlemstep  10508  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2z  10515  btwnzge0  10561  iseqf1olemqf1o  10769  mulexpzap  10842  leexp1a  10857  hashen  11047  fihashdom  11067  hashun  11069  swrdccatin1  11310  pfxccatin12lem3  11317  pfxccat3  11319  cjap  11484  cvg1nlemres  11563  rsqrmo  11605  abslt  11666  abs3lem  11689  cau3lem  11692  rexanre  11798  xrmaxltsup  11836  climcau  11925  sumeq2  11937  summodc  11962  fisumss  11971  fsum2d  12014  fsumabs  12044  fsumiun  12056  prodeq2  12136  prodmodclem2  12156  fprodcl2lem  12184  fprodap0  12200  fprod2d  12202  fprodrec  12208  fprodap0f  12215  fprodle  12219  eirrap  12357  divalglemeunn  12500  divalglemeuneg  12502  bezoutlemnewy  12585  bezoutlemstep  12586  bezoutlemmain  12587  bezoutlembi  12594  bezoutlemeu  12596  qredeu  12687  isprm5lem  12731  pw2dvdseu  12758  sqrt2irrap  12770  pythagtriplem2  12857  pythagtrip  12874  pclemub  12878  pcqmul  12894  pcexp  12900  pcneg  12916  pcprmpw2  12924  pcadd  12931  prmpwdvds  12946  4sqlem13m  12994  ennnfonelemg  13042  ennnfonelemrnh  13055  ctiunctlemfo  13078  nninfdclemf1  13091  imasival  13407  sgrppropd  13514  ismndd  13538  mndpropd  13541  mhmeql  13593  mhmmnd  13721  mulgfng  13729  issubg4m  13798  ssnmz  13816  conjnmzb  13885  rngpropd  13987  ringpropd  14070  dvdsrtr  14134  islmod  14324  mplsubgfilemcl  14732  restbasg  14911  cnpnei  14962  cnptoprest2  14983  cnpdis  14985  lmtopcnp  14993  txcnp  15014  ismet2  15097  blininf  15167  metss2lem  15240  xmettxlem  15252  xmettx  15253  metcnp  15255  metcnpi3  15260  addcncntoplem  15304  fsumcncntop  15310  mulc1cncf  15332  cncfco  15334  mulcncf  15351  dedekindeulemuub  15360  dedekindeu  15366  dedekindicclemuub  15369  ivthinclemloc  15384  ivthinc  15386  limcimo  15408  limccnp2cntop  15420  dveflem  15469  plyf  15480  plyco  15502  plycj  15504  dvply2g  15509  logbgcd1irrap  15713  perfectlem2  15743  lgsdilem  15775  lgsquad2lem2  15830  lgsquad3  15832  2sqlem5  15867  2sqlem9  15872  usgredg4  16085  usgr1eop  16115  usgr1vr  16118  subuhgr  16142  subumgr  16144  subusgr  16145  clwwlknonex2lem2  16308  2omap  16645  pw1map  16647  qdencn  16682  apdiff  16703  qdiff  16704  gfsumval  16732