Theorem simplrl 525

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 108	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	ad2antlr 481	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  rmob  3042  disjiun  3976  f1imass  5741  riota5f  5821  tfrexlem  6298  tfrcl  6328  nnsucuniel  6459  nntr2  6467  fopwdom  6798  fidceq  6831  fisbth  6845  fientri3  6876  unsnfidcex  6881  undifdc  6885  iunfidisj  6907  fiuni  6939  ordiso2  6996  acfun  7159  ccfunen  7201  addcmpblnq  7304  mulcmpblnq  7305  ordpipqqs  7311  addcmpblnq0  7380  mulcmpblnq0  7381  prml  7414  addlocpr  7473  prmuloc  7503  mullocpr  7508  ltexprlemopl  7538  ltexprlemopu  7540  ltexprlemloc  7544  ltexprlemrl  7547  ltexprlemru  7549  addcanprleml  7551  addcanprlemu  7552  aptiprleml  7576  ltmprr  7579  cauappcvgprlemopl  7583  cauappcvgprlemopu  7585  cauappcvgprlemloc  7589  caucvgprlemopl  7606  caucvgprlemopu  7608  caucvgprlemloc  7612  caucvgprprlemopu  7636  caucvgprprlemloc  7640  caucvgprprlemexbt  7643  caucvgprprlemaddq  7645  suplocexprlemrl  7654  suplocexprlemdisj  7657  suplocexprlemloc  7658  suplocexprlemub  7660  addcmpblnr  7676  mulcmpblnrlemg  7677  mulcmpblnr  7678  ltsrprg  7684  mulgt0sr  7715  caucvgsrlemgt1  7732  suplocsrlemb  7743  axmulcl  7803  axcaucvglemres  7836  axpre-suploclemres  7838  axpre-suploc  7839  cnegexlem1  8069  negeu  8085  add20  8368  apreap  8481  cru  8496  apsym  8500  apcotr  8501  apadd1  8502  apneg  8505  mulext1  8506  mulge0  8513  mulap0  8547  divdivdivap  8605  prodgt0  8743  ltmul12a  8751  lt2mul2div  8770  ledivdiv  8781  lediv12a  8785  qapne  9573  xleadd1a  9805  ixxss12  9838  elfz0ubfz0  10056  qtri3or  10174  exbtwnzlemstep  10179  exbtwnzlemex  10181  exbtwnz  10182  rebtwn2zlemstep  10184  rebtwn2z  10186  btwnzge0  10231  iseqf1olemqf1o  10424  mulexpzap  10491  leexp1a  10506  hashen  10693  fihashdom  10712  hashun  10714  cjap  10844  cvg1nlemres  10923  rsqrmo  10965  abslt  11026  abs3lem  11049  cau3lem  11052  rexanre  11158  xrmaxltsup  11195  climcau  11284  sumeq2  11296  summodc  11320  fisumss  11329  fsum2d  11372  fsumabs  11402  fsumiun  11414  prodeq2  11494  prodmodclem2  11514  fprodcl2lem  11542  fprodap0  11558  fprod2d  11560  fprodrec  11566  fprodap0f  11573  fprodle  11577  eirrap  11714  divalglemeunn  11854  divalglemeuneg  11856  bezoutlemnewy  11925  bezoutlemstep  11926  bezoutlemmain  11927  bezoutlembi  11934  bezoutlemeu  11936  qredeu  12025  isprm5lem  12069  pw2dvdseu  12096  sqrt2irrap  12108  pythagtriplem2  12194  pythagtrip  12211  pclemub  12215  pcqmul  12231  pcexp  12237  pcneg  12252  pcprmpw2  12260  pcadd  12267  prmpwdvds  12281  ennnfonelemg  12332  ennnfonelemrnh  12345  ctiunctlemfo  12368  nninfdclemf1  12381  restbasg  12768  cnpnei  12819  cnptoprest2  12840  cnpdis  12842  lmtopcnp  12850  txcnp  12871  ismet2  12954  blininf  13024  metss2lem  13097  xmettxlem  13109  xmettx  13110  metcnp  13112  metcnpi3  13117  addcncntoplem  13151  fsumcncntop  13156  mulc1cncf  13176  cncfco  13178  mulcncf  13191  dedekindeulemuub  13195  dedekindeu  13201  dedekindicclemuub  13204  ivthinclemloc  13219  ivthinc  13221  limcimo  13234  limccnp2cntop  13246  dveflem  13287  logbgcd1irrap  13488  lgsdilem  13528  2sqlem5  13555  2sqlem9  13560  qdencn  13866  apdiff  13887