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  3090  disjiun  4038  f1imass  5842  riota5f  5923  tfrexlem  6419  tfrcl  6449  nnsucuniel  6580  nntr2  6588  pw2f1odclem  6930  fopwdom  6932  fidceq  6965  fisbth  6979  fientri3  7011  unsnfidcex  7016  undifdc  7020  iunfidisj  7047  fiuni  7079  ordiso2  7136  nninfninc  7224  acfun  7318  2omotaplemap  7368  ccfunen  7375  addcmpblnq  7479  mulcmpblnq  7480  ordpipqqs  7486  addcmpblnq0  7555  mulcmpblnq0  7556  prml  7589  addlocpr  7648  prmuloc  7678  mullocpr  7683  ltexprlemopl  7713  ltexprlemopu  7715  ltexprlemloc  7719  ltexprlemrl  7722  ltexprlemru  7724  addcanprleml  7726  addcanprlemu  7727  aptiprleml  7751  ltmprr  7754  cauappcvgprlemopl  7758  cauappcvgprlemopu  7760  cauappcvgprlemloc  7764  caucvgprlemopl  7781  caucvgprlemopu  7783  caucvgprlemloc  7787  caucvgprprlemopu  7811  caucvgprprlemloc  7815  caucvgprprlemexbt  7818  caucvgprprlemaddq  7820  suplocexprlemrl  7829  suplocexprlemdisj  7832  suplocexprlemloc  7833  suplocexprlemub  7835  addcmpblnr  7851  mulcmpblnrlemg  7852  mulcmpblnr  7853  ltsrprg  7859  mulgt0sr  7890  caucvgsrlemgt1  7907  suplocsrlemb  7918  axmulcl  7978  axcaucvglemres  8011  axpre-suploclemres  8013  axpre-suploc  8014  cnegexlem1  8246  negeu  8262  add20  8546  apreap  8659  cru  8674  apsym  8678  apcotr  8679  apadd1  8680  apneg  8683  mulext1  8684  mulge0  8691  mulap0  8726  divdivdivap  8785  prodgt0  8924  ltmul12a  8932  lt2mul2div  8951  ledivdiv  8962  lediv12a  8966  qapne  9759  xleadd1a  9994  ixxss12  10027  elfz0ubfz0  10246  qtri3or  10381  exbtwnzlemstep  10388  exbtwnzlemex  10390  exbtwnz  10391  rebtwn2zlemstep  10393  rebtwn2z  10395  btwnzge0  10441  iseqf1olemqf1o  10649  mulexpzap  10722  leexp1a  10737  hashen  10927  fihashdom  10946  hashun  10948  cjap  11188  cvg1nlemres  11267  rsqrmo  11309  abslt  11370  abs3lem  11393  cau3lem  11396  rexanre  11502  xrmaxltsup  11540  climcau  11629  sumeq2  11641  summodc  11665  fisumss  11674  fsum2d  11717  fsumabs  11747  fsumiun  11759  prodeq2  11839  prodmodclem2  11859  fprodcl2lem  11887  fprodap0  11903  fprod2d  11905  fprodrec  11911  fprodap0f  11918  fprodle  11922  eirrap  12060  divalglemeunn  12203  divalglemeuneg  12205  bezoutlemnewy  12288  bezoutlemstep  12289  bezoutlemmain  12290  bezoutlembi  12297  bezoutlemeu  12299  qredeu  12390  isprm5lem  12434  pw2dvdseu  12461  sqrt2irrap  12473  pythagtriplem2  12560  pythagtrip  12577  pclemub  12581  pcqmul  12597  pcexp  12603  pcneg  12619  pcprmpw2  12627  pcadd  12634  prmpwdvds  12649  4sqlem13m  12697  ennnfonelemg  12745  ennnfonelemrnh  12758  ctiunctlemfo  12781  nninfdclemf1  12794  imasival  13109  sgrppropd  13216  ismndd  13240  mndpropd  13243  mhmeql  13295  mhmmnd  13423  mulgfng  13431  issubg4m  13500  ssnmz  13518  conjnmzb  13587  rngpropd  13688  ringpropd  13771  dvdsrtr  13834  islmod  14024  mplsubgfilemcl  14432  restbasg  14611  cnpnei  14662  cnptoprest2  14683  cnpdis  14685  lmtopcnp  14693  txcnp  14714  ismet2  14797  blininf  14867  metss2lem  14940  xmettxlem  14952  xmettx  14953  metcnp  14955  metcnpi3  14960  addcncntoplem  15004  fsumcncntop  15010  mulc1cncf  15032  cncfco  15034  mulcncf  15051  dedekindeulemuub  15060  dedekindeu  15066  dedekindicclemuub  15069  ivthinclemloc  15084  ivthinc  15086  limcimo  15108  limccnp2cntop  15120  dveflem  15169  plyf  15180  plyco  15202  plycj  15204  dvply2g  15209  logbgcd1irrap  15413  perfectlem2  15443  lgsdilem  15475  lgsquad2lem2  15530  lgsquad3  15532  2sqlem5  15567  2sqlem9  15572  2omap  15894  qdencn  15928  apdiff  15949