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  3095  disjiun  4049  f1imass  5861  riota5f  5942  tfrexlem  6438  tfrcl  6468  nnsucuniel  6599  nntr2  6607  pw2f1odclem  6951  fopwdom  6953  fidceq  6987  fisbth  7001  fientri3  7033  unsnfidcex  7038  undifdc  7042  iunfidisj  7069  fiuni  7101  ordiso2  7158  nninfninc  7246  acfun  7345  2omotaplemap  7399  ccfunen  7406  addcmpblnq  7510  mulcmpblnq  7511  ordpipqqs  7517  addcmpblnq0  7586  mulcmpblnq0  7587  prml  7620  addlocpr  7679  prmuloc  7709  mullocpr  7714  ltexprlemopl  7744  ltexprlemopu  7746  ltexprlemloc  7750  ltexprlemrl  7753  ltexprlemru  7755  addcanprleml  7757  addcanprlemu  7758  aptiprleml  7782  ltmprr  7785  cauappcvgprlemopl  7789  cauappcvgprlemopu  7791  cauappcvgprlemloc  7795  caucvgprlemopl  7812  caucvgprlemopu  7814  caucvgprlemloc  7818  caucvgprprlemopu  7842  caucvgprprlemloc  7846  caucvgprprlemexbt  7849  caucvgprprlemaddq  7851  suplocexprlemrl  7860  suplocexprlemdisj  7863  suplocexprlemloc  7864  suplocexprlemub  7866  addcmpblnr  7882  mulcmpblnrlemg  7883  mulcmpblnr  7884  ltsrprg  7890  mulgt0sr  7921  caucvgsrlemgt1  7938  suplocsrlemb  7949  axmulcl  8009  axcaucvglemres  8042  axpre-suploclemres  8044  axpre-suploc  8045  cnegexlem1  8277  negeu  8293  add20  8577  apreap  8690  cru  8705  apsym  8709  apcotr  8710  apadd1  8711  apneg  8714  mulext1  8715  mulge0  8722  mulap0  8757  divdivdivap  8816  prodgt0  8955  ltmul12a  8963  lt2mul2div  8982  ledivdiv  8993  lediv12a  8997  qapne  9790  xleadd1a  10025  ixxss12  10058  elfz0ubfz0  10277  qtri3or  10415  exbtwnzlemstep  10422  exbtwnzlemex  10424  exbtwnz  10425  rebtwn2zlemstep  10427  rebtwn2z  10429  btwnzge0  10475  iseqf1olemqf1o  10683  mulexpzap  10756  leexp1a  10771  hashen  10961  fihashdom  10980  hashun  10982  cjap  11302  cvg1nlemres  11381  rsqrmo  11423  abslt  11484  abs3lem  11507  cau3lem  11510  rexanre  11616  xrmaxltsup  11654  climcau  11743  sumeq2  11755  summodc  11779  fisumss  11788  fsum2d  11831  fsumabs  11861  fsumiun  11873  prodeq2  11953  prodmodclem2  11973  fprodcl2lem  12001  fprodap0  12017  fprod2d  12019  fprodrec  12025  fprodap0f  12032  fprodle  12036  eirrap  12174  divalglemeunn  12317  divalglemeuneg  12319  bezoutlemnewy  12402  bezoutlemstep  12403  bezoutlemmain  12404  bezoutlembi  12411  bezoutlemeu  12413  qredeu  12504  isprm5lem  12548  pw2dvdseu  12575  sqrt2irrap  12587  pythagtriplem2  12674  pythagtrip  12691  pclemub  12695  pcqmul  12711  pcexp  12717  pcneg  12733  pcprmpw2  12741  pcadd  12748  prmpwdvds  12763  4sqlem13m  12811  ennnfonelemg  12859  ennnfonelemrnh  12872  ctiunctlemfo  12895  nninfdclemf1  12908  imasival  13223  sgrppropd  13330  ismndd  13354  mndpropd  13357  mhmeql  13409  mhmmnd  13537  mulgfng  13545  issubg4m  13614  ssnmz  13632  conjnmzb  13701  rngpropd  13802  ringpropd  13885  dvdsrtr  13948  islmod  14138  mplsubgfilemcl  14546  restbasg  14725  cnpnei  14776  cnptoprest2  14797  cnpdis  14799  lmtopcnp  14807  txcnp  14828  ismet2  14911  blininf  14981  metss2lem  15054  xmettxlem  15066  xmettx  15067  metcnp  15069  metcnpi3  15074  addcncntoplem  15118  fsumcncntop  15124  mulc1cncf  15146  cncfco  15148  mulcncf  15165  dedekindeulemuub  15174  dedekindeu  15180  dedekindicclemuub  15183  ivthinclemloc  15198  ivthinc  15200  limcimo  15222  limccnp2cntop  15234  dveflem  15283  plyf  15294  plyco  15316  plycj  15318  dvply2g  15323  logbgcd1irrap  15527  perfectlem2  15557  lgsdilem  15589  lgsquad2lem2  15644  lgsquad3  15646  2sqlem5  15681  2sqlem9  15686  2omap  16102  pw1map  16104  qdencn  16138  apdiff  16159