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  3136  disjiun  4104  f1imass  5947  riota5f  6030  tfrexlem  6565  tfrcl  6595  nnsucuniel  6728  nntr2  6736  pw2f1odclem  7087  fopwdom  7089  fidceq  7124  fisbth  7140  fidcen  7156  fientri3  7175  unsnfidcex  7180  undifdc  7184  iunfidisj  7213  fiuni  7265  2omap  7269  ordiso2  7326  nninfninc  7414  acfun  7514  2omotaplemap  7571  ccfunen  7578  addcmpblnq  7682  mulcmpblnq  7683  ordpipqqs  7689  addcmpblnq0  7758  mulcmpblnq0  7759  prml  7792  addlocpr  7851  prmuloc  7881  mullocpr  7886  ltexprlemopl  7916  ltexprlemopu  7918  ltexprlemloc  7922  ltexprlemrl  7925  ltexprlemru  7927  addcanprleml  7929  addcanprlemu  7930  aptiprleml  7954  ltmprr  7957  cauappcvgprlemopl  7961  cauappcvgprlemopu  7963  cauappcvgprlemloc  7967  caucvgprlemopl  7984  caucvgprlemopu  7986  caucvgprlemloc  7990  caucvgprprlemopu  8014  caucvgprprlemloc  8018  caucvgprprlemexbt  8021  caucvgprprlemaddq  8023  suplocexprlemrl  8032  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemub  8038  addcmpblnr  8054  mulcmpblnrlemg  8055  mulcmpblnr  8056  ltsrprg  8062  mulgt0sr  8093  caucvgsrlemgt1  8110  suplocsrlemb  8121  axmulcl  8181  axcaucvglemres  8214  axpre-suploclemres  8216  axpre-suploc  8217  cnegexlem1  8448  negeu  8464  add20  8748  apreap  8861  cru  8876  apsym  8880  apcotr  8881  apadd1  8882  apneg  8885  mulext1  8886  mulge0  8893  mulap0  8928  divdivdivap  8987  prodgt0  9126  ltmul12a  9134  lt2mul2div  9153  ledivdiv  9164  lediv12a  9168  qapne  9971  xleadd1a  10206  ixxss12  10239  elfz0ubfz0  10459  qtri3or  10600  exbtwnzlemstep  10607  exbtwnzlemex  10609  exbtwnz  10610  rebtwn2zlemstep  10612  rebtwn2z  10614  btwnzge0  10660  iseqf1olemqf1o  10868  mulexpzap  10941  leexp1a  10956  hashen  11147  fihashdom  11167  hashun  11169  swrdccatin1  11417  pfxccatin12lem3  11424  pfxccat3  11426  cjap  11591  cvg1nlemres  11670  rsqrmo  11712  abslt  11773  abs3lem  11796  cau3lem  11799  rexanre  11905  xrmaxltsup  11943  climcau  12032  sumeq2  12044  summodc  12069  fisumss  12078  fsum2d  12121  fsumabs  12151  fsumiun  12163  prodeq2  12243  prodmodclem2  12263  fprodcl2lem  12291  fprodap0  12307  fprod2d  12309  fprodrec  12315  fprodap0f  12322  fprodle  12326  eirrap  12464  divalglemeunn  12607  divalglemeuneg  12609  bezoutlemnewy  12692  bezoutlemstep  12693  bezoutlemmain  12694  bezoutlembi  12701  bezoutlemeu  12703  qredeu  12794  isprm5lem  12838  pw2dvdseu  12865  sqrt2irrap  12877  pythagtriplem2  12964  pythagtrip  12981  pclemub  12985  pcqmul  13001  pcexp  13007  pcneg  13023  pcprmpw2  13031  pcadd  13038  prmpwdvds  13053  4sqlem13m  13101  ennnfonelemg  13154  ennnfonelemrnh  13167  ctiunctlemfo  13190  nninfdclemf1  13203  imasival  13519  sgrppropd  13626  ismndd  13650  mndpropd  13653  mhmeql  13705  mhmmnd  13833  mulgfng  13841  issubg4m  13910  ssnmz  13928  conjnmzb  13997  rngpropd  14099  ringpropd  14182  dvdsrtr  14246  aprlring  14434  islmod  14439  mplsubgfilemcl  14854  restbasg  15033  cnpnei  15084  cnptoprest2  15105  cnpdis  15107  lmtopcnp  15115  txcnp  15136  ismet2  15219  blininf  15289  metss2lem  15362  xmettxlem  15374  xmettx  15375  metcnp  15377  metcnpi3  15382  addcncntoplem  15426  fsumcncntop  15432  mulc1cncf  15454  cncfco  15456  mulcncf  15473  dedekindeulemuub  15482  dedekindeu  15488  dedekindicclemuub  15491  ivthinclemloc  15506  ivthinc  15508  limcimo  15530  limccnp2cntop  15542  dveflem  15591  plyf  15602  plyco  15624  plycj  15626  dvply2g  15631  logbgcd1irrap  15835  perfectlem2  15868  lgsdilem  15900  lgsquad2lem2  15955  lgsquad3  15957  2sqlem5  15992  2sqlem9  15997  usgredg4  16210  usgr1eop  16240  usgr1vr  16243  subuhgr  16267  subumgr  16269  subusgr  16270  clwwlknonex2lem2  16433  pw1map  16769  qdencn  16807  apdiff  16832  qdiff  16833  gfsumval  16862