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  3070  disjiun  4016  f1imass  5799  riota5f  5880  tfrexlem  6363  tfrcl  6393  nnsucuniel  6524  nntr2  6532  pw2f1odclem  6866  fopwdom  6868  fidceq  6901  fisbth  6915  fientri3  6947  unsnfidcex  6952  undifdc  6956  iunfidisj  6979  fiuni  7011  ordiso2  7068  nninfninc  7156  acfun  7241  2omotaplemap  7291  ccfunen  7298  addcmpblnq  7401  mulcmpblnq  7402  ordpipqqs  7408  addcmpblnq0  7477  mulcmpblnq0  7478  prml  7511  addlocpr  7570  prmuloc  7600  mullocpr  7605  ltexprlemopl  7635  ltexprlemopu  7637  ltexprlemloc  7641  ltexprlemrl  7644  ltexprlemru  7646  addcanprleml  7648  addcanprlemu  7649  aptiprleml  7673  ltmprr  7676  cauappcvgprlemopl  7680  cauappcvgprlemopu  7682  cauappcvgprlemloc  7686  caucvgprlemopl  7703  caucvgprlemopu  7705  caucvgprlemloc  7709  caucvgprprlemopu  7733  caucvgprprlemloc  7737  caucvgprprlemexbt  7740  caucvgprprlemaddq  7742  suplocexprlemrl  7751  suplocexprlemdisj  7754  suplocexprlemloc  7755  suplocexprlemub  7757  addcmpblnr  7773  mulcmpblnrlemg  7774  mulcmpblnr  7775  ltsrprg  7781  mulgt0sr  7812  caucvgsrlemgt1  7829  suplocsrlemb  7840  axmulcl  7900  axcaucvglemres  7933  axpre-suploclemres  7935  axpre-suploc  7936  cnegexlem1  8167  negeu  8183  add20  8466  apreap  8579  cru  8594  apsym  8598  apcotr  8599  apadd1  8600  apneg  8603  mulext1  8604  mulge0  8611  mulap0  8646  divdivdivap  8705  prodgt0  8844  ltmul12a  8852  lt2mul2div  8871  ledivdiv  8882  lediv12a  8886  qapne  9675  xleadd1a  9909  ixxss12  9942  elfz0ubfz0  10161  qtri3or  10279  exbtwnzlemstep  10284  exbtwnzlemex  10286  exbtwnz  10287  rebtwn2zlemstep  10289  rebtwn2z  10291  btwnzge0  10337  iseqf1olemqf1o  10532  mulexpzap  10600  leexp1a  10615  hashen  10805  fihashdom  10824  hashun  10826  cjap  10956  cvg1nlemres  11035  rsqrmo  11077  abslt  11138  abs3lem  11161  cau3lem  11164  rexanre  11270  xrmaxltsup  11307  climcau  11396  sumeq2  11408  summodc  11432  fisumss  11441  fsum2d  11484  fsumabs  11514  fsumiun  11526  prodeq2  11606  prodmodclem2  11626  fprodcl2lem  11654  fprodap0  11670  fprod2d  11672  fprodrec  11678  fprodap0f  11685  fprodle  11689  eirrap  11826  divalglemeunn  11967  divalglemeuneg  11969  bezoutlemnewy  12038  bezoutlemstep  12039  bezoutlemmain  12040  bezoutlembi  12047  bezoutlemeu  12049  qredeu  12140  isprm5lem  12184  pw2dvdseu  12211  sqrt2irrap  12223  pythagtriplem2  12309  pythagtrip  12326  pclemub  12330  pcqmul  12346  pcexp  12352  pcneg  12368  pcprmpw2  12376  pcadd  12383  prmpwdvds  12398  4sqlem13m  12446  ennnfonelemg  12465  ennnfonelemrnh  12478  ctiunctlemfo  12501  nninfdclemf1  12514  imasival  12794  sgrppropd  12899  ismndd  12921  mndpropd  12924  mhmeql  12967  mhmmnd  13081  mulgfng  13089  issubg4m  13157  ssnmz  13175  conjnmzb  13244  rngpropd  13334  ringpropd  13417  dvdsrtr  13476  islmod  13632  restbasg  14153  cnpnei  14204  cnptoprest2  14225  cnpdis  14227  lmtopcnp  14235  txcnp  14256  ismet2  14339  blininf  14409  metss2lem  14482  xmettxlem  14494  xmettx  14495  metcnp  14497  metcnpi3  14502  addcncntoplem  14536  fsumcncntop  14541  mulc1cncf  14561  cncfco  14563  mulcncf  14576  dedekindeulemuub  14580  dedekindeu  14586  dedekindicclemuub  14589  ivthinclemloc  14604  ivthinc  14606  limcimo  14619  limccnp2cntop  14631  dveflem  14672  logbgcd1irrap  14873  lgsdilem  14914  2sqlem5  14952  2sqlem9  14957  qdencn  15263  apdiff  15284