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  3053  disjiun  3993  f1imass  5765  riota5f  5845  tfrexlem  6325  tfrcl  6355  nnsucuniel  6486  nntr2  6494  fopwdom  6826  fidceq  6859  fisbth  6873  fientri3  6904  unsnfidcex  6909  undifdc  6913  iunfidisj  6935  fiuni  6967  ordiso2  7024  acfun  7196  ccfunen  7238  addcmpblnq  7341  mulcmpblnq  7342  ordpipqqs  7348  addcmpblnq0  7417  mulcmpblnq0  7418  prml  7451  addlocpr  7510  prmuloc  7540  mullocpr  7545  ltexprlemopl  7575  ltexprlemopu  7577  ltexprlemloc  7581  ltexprlemrl  7584  ltexprlemru  7586  addcanprleml  7588  addcanprlemu  7589  aptiprleml  7613  ltmprr  7616  cauappcvgprlemopl  7620  cauappcvgprlemopu  7622  cauappcvgprlemloc  7626  caucvgprlemopl  7643  caucvgprlemopu  7645  caucvgprlemloc  7649  caucvgprprlemopu  7673  caucvgprprlemloc  7677  caucvgprprlemexbt  7680  caucvgprprlemaddq  7682  suplocexprlemrl  7691  suplocexprlemdisj  7694  suplocexprlemloc  7695  suplocexprlemub  7697  addcmpblnr  7713  mulcmpblnrlemg  7714  mulcmpblnr  7715  ltsrprg  7721  mulgt0sr  7752  caucvgsrlemgt1  7769  suplocsrlemb  7780  axmulcl  7840  axcaucvglemres  7873  axpre-suploclemres  7875  axpre-suploc  7876  cnegexlem1  8106  negeu  8122  add20  8405  apreap  8518  cru  8533  apsym  8537  apcotr  8538  apadd1  8539  apneg  8542  mulext1  8543  mulge0  8550  mulap0  8584  divdivdivap  8643  prodgt0  8782  ltmul12a  8790  lt2mul2div  8809  ledivdiv  8820  lediv12a  8824  qapne  9612  xleadd1a  9844  ixxss12  9877  elfz0ubfz0  10095  qtri3or  10213  exbtwnzlemstep  10218  exbtwnzlemex  10220  exbtwnz  10221  rebtwn2zlemstep  10223  rebtwn2z  10225  btwnzge0  10270  iseqf1olemqf1o  10463  mulexpzap  10530  leexp1a  10545  hashen  10732  fihashdom  10751  hashun  10753  cjap  10883  cvg1nlemres  10962  rsqrmo  11004  abslt  11065  abs3lem  11088  cau3lem  11091  rexanre  11197  xrmaxltsup  11234  climcau  11323  sumeq2  11335  summodc  11359  fisumss  11368  fsum2d  11411  fsumabs  11441  fsumiun  11453  prodeq2  11533  prodmodclem2  11553  fprodcl2lem  11581  fprodap0  11597  fprod2d  11599  fprodrec  11605  fprodap0f  11612  fprodle  11616  eirrap  11753  divalglemeunn  11893  divalglemeuneg  11895  bezoutlemnewy  11964  bezoutlemstep  11965  bezoutlemmain  11966  bezoutlembi  11973  bezoutlemeu  11975  qredeu  12064  isprm5lem  12108  pw2dvdseu  12135  sqrt2irrap  12147  pythagtriplem2  12233  pythagtrip  12250  pclemub  12254  pcqmul  12270  pcexp  12276  pcneg  12291  pcprmpw2  12299  pcadd  12306  prmpwdvds  12320  ennnfonelemg  12371  ennnfonelemrnh  12384  ctiunctlemfo  12407  nninfdclemf1  12420  ismndd  12713  mndpropd  12716  mhmeql  12747  mhmmnd  12850  mulgfng  12857  ringpropd  13022  restbasg  13248  cnpnei  13299  cnptoprest2  13320  cnpdis  13322  lmtopcnp  13330  txcnp  13351  ismet2  13434  blininf  13504  metss2lem  13577  xmettxlem  13589  xmettx  13590  metcnp  13592  metcnpi3  13597  addcncntoplem  13631  fsumcncntop  13636  mulc1cncf  13656  cncfco  13658  mulcncf  13671  dedekindeulemuub  13675  dedekindeu  13681  dedekindicclemuub  13684  ivthinclemloc  13699  ivthinc  13701  limcimo  13714  limccnp2cntop  13726  dveflem  13767  logbgcd1irrap  13968  lgsdilem  14008  2sqlem5  14035  2sqlem9  14040  qdencn  14345  apdiff  14366