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  3123  disjiun  4081  f1imass  5910  riota5f  5993  tfrexlem  6495  tfrcl  6525  nnsucuniel  6658  nntr2  6666  pw2f1odclem  7015  fopwdom  7017  fidceq  7051  fisbth  7065  fidcen  7081  fientri3  7100  unsnfidcex  7105  undifdc  7109  iunfidisj  7136  fiuni  7168  ordiso2  7225  nninfninc  7313  acfun  7412  2omotaplemap  7466  ccfunen  7473  addcmpblnq  7577  mulcmpblnq  7578  ordpipqqs  7584  addcmpblnq0  7653  mulcmpblnq0  7654  prml  7687  addlocpr  7746  prmuloc  7776  mullocpr  7781  ltexprlemopl  7811  ltexprlemopu  7813  ltexprlemloc  7817  ltexprlemrl  7820  ltexprlemru  7822  addcanprleml  7824  addcanprlemu  7825  aptiprleml  7849  ltmprr  7852  cauappcvgprlemopl  7856  cauappcvgprlemopu  7858  cauappcvgprlemloc  7862  caucvgprlemopl  7879  caucvgprlemopu  7881  caucvgprlemloc  7885  caucvgprprlemopu  7909  caucvgprprlemloc  7913  caucvgprprlemexbt  7916  caucvgprprlemaddq  7918  suplocexprlemrl  7927  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemub  7933  addcmpblnr  7949  mulcmpblnrlemg  7950  mulcmpblnr  7951  ltsrprg  7957  mulgt0sr  7988  caucvgsrlemgt1  8005  suplocsrlemb  8016  axmulcl  8076  axcaucvglemres  8109  axpre-suploclemres  8111  axpre-suploc  8112  cnegexlem1  8344  negeu  8360  add20  8644  apreap  8757  cru  8772  apsym  8776  apcotr  8777  apadd1  8778  apneg  8781  mulext1  8782  mulge0  8789  mulap0  8824  divdivdivap  8883  prodgt0  9022  ltmul12a  9030  lt2mul2div  9049  ledivdiv  9060  lediv12a  9064  qapne  9863  xleadd1a  10098  ixxss12  10131  elfz0ubfz0  10350  qtri3or  10490  exbtwnzlemstep  10497  exbtwnzlemex  10499  exbtwnz  10500  rebtwn2zlemstep  10502  rebtwn2z  10504  btwnzge0  10550  iseqf1olemqf1o  10758  mulexpzap  10831  leexp1a  10846  hashen  11036  fihashdom  11056  hashun  11058  swrdccatin1  11296  pfxccatin12lem3  11303  pfxccat3  11305  cjap  11457  cvg1nlemres  11536  rsqrmo  11578  abslt  11639  abs3lem  11662  cau3lem  11665  rexanre  11771  xrmaxltsup  11809  climcau  11898  sumeq2  11910  summodc  11934  fisumss  11943  fsum2d  11986  fsumabs  12016  fsumiun  12028  prodeq2  12108  prodmodclem2  12128  fprodcl2lem  12156  fprodap0  12172  fprod2d  12174  fprodrec  12180  fprodap0f  12187  fprodle  12191  eirrap  12329  divalglemeunn  12472  divalglemeuneg  12474  bezoutlemnewy  12557  bezoutlemstep  12558  bezoutlemmain  12559  bezoutlembi  12566  bezoutlemeu  12568  qredeu  12659  isprm5lem  12703  pw2dvdseu  12730  sqrt2irrap  12742  pythagtriplem2  12829  pythagtrip  12846  pclemub  12850  pcqmul  12866  pcexp  12872  pcneg  12888  pcprmpw2  12896  pcadd  12903  prmpwdvds  12918  4sqlem13m  12966  ennnfonelemg  13014  ennnfonelemrnh  13027  ctiunctlemfo  13050  nninfdclemf1  13063  imasival  13379  sgrppropd  13486  ismndd  13510  mndpropd  13513  mhmeql  13565  mhmmnd  13693  mulgfng  13701  issubg4m  13770  ssnmz  13788  conjnmzb  13857  rngpropd  13958  ringpropd  14041  dvdsrtr  14105  islmod  14295  mplsubgfilemcl  14703  restbasg  14882  cnpnei  14933  cnptoprest2  14954  cnpdis  14956  lmtopcnp  14964  txcnp  14985  ismet2  15068  blininf  15138  metss2lem  15211  xmettxlem  15223  xmettx  15224  metcnp  15226  metcnpi3  15231  addcncntoplem  15275  fsumcncntop  15281  mulc1cncf  15303  cncfco  15305  mulcncf  15322  dedekindeulemuub  15331  dedekindeu  15337  dedekindicclemuub  15340  ivthinclemloc  15355  ivthinc  15357  limcimo  15379  limccnp2cntop  15391  dveflem  15440  plyf  15451  plyco  15473  plycj  15475  dvply2g  15480  logbgcd1irrap  15684  perfectlem2  15714  lgsdilem  15746  lgsquad2lem2  15801  lgsquad3  15803  2sqlem5  15838  2sqlem9  15843  usgredg4  16054  usgr1eop  16084  usgr1vr  16087  clwwlknonex2lem2  16233  2omap  16530  pw1map  16532  qdencn  16567  apdiff  16588