Theorem simplrl 537

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  3139  disjiun  4109  f1imass  5953  riota5f  6038  tfrexlem  6578  tfrcl  6608  nnsucuniel  6741  nntr2  6749  pw2f1odclem  7100  fopwdom  7102  fidceq  7137  fisbth  7153  fidcen  7169  fientri3  7188  unsnfidcex  7193  undifdc  7197  iunfidisj  7226  fiuni  7278  2omap  7282  ordiso2  7339  nninfninc  7427  acfun  7527  2omotaplemap  7587  ccfunen  7594  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  addcmpblnq0  7774  mulcmpblnq0  7775  prml  7808  addlocpr  7867  prmuloc  7897  mullocpr  7902  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemloc  7938  ltexprlemrl  7941  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  aptiprleml  7970  ltmprr  7973  cauappcvgprlemopl  7977  cauappcvgprlemopu  7979  cauappcvgprlemloc  7983  caucvgprlemopl  8000  caucvgprlemopu  8002  caucvgprlemloc  8006  caucvgprprlemopu  8030  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  caucvgprprlemaddq  8039  suplocexprlemrl  8048  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  ltsrprg  8078  mulgt0sr  8109  caucvgsrlemgt1  8126  suplocsrlemb  8137  axmulcl  8197  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  cnegexlem1  8464  negeu  8480  add20  8765  apreap  8878  cru  8893  apsym  8897  apcotr  8898  apadd1  8899  apneg  8902  mulext1  8903  mulge0  8910  mulap0  8945  divdivdivap  9004  prodgt0  9143  ltmul12a  9151  lt2mul2div  9170  ledivdiv  9181  lediv12a  9185  qapne  9989  xleadd1a  10225  ixxss12  10258  elfz0ubfz0  10481  qtri3or  10624  exbtwnzlemstep  10631  exbtwnzlemex  10633  exbtwnz  10634  rebtwn2zlemstep  10636  rebtwn2z  10638  btwnzge0  10684  iseqf1olemqf1o  10892  mulexpzap  10965  leexp1a  10980  hashen  11172  fihashdom  11192  hashun  11194  swrdccatin1  11442  pfxccatin12lem3  11449  pfxccat3  11451  cjap  11616  cvg1nlemres  11695  rsqrmo  11737  abslt  11798  abs3lem  11821  cau3lem  11824  rexanre  11930  xrmaxltsup  11968  climcau  12057  sumeq2  12069  summodc  12094  fisumss  12103  fsum2d  12146  fsumabs  12176  fsumiun  12188  prodeq2  12268  prodmodclem2  12288  fprodcl2lem  12316  fprodap0  12332  fprod2d  12334  fprodrec  12340  fprodap0f  12347  fprodle  12351  eirrap  12489  divalglemeunn  12632  divalglemeuneg  12634  bezoutlemnewy  12717  bezoutlemstep  12718  bezoutlemmain  12719  bezoutlembi  12726  bezoutlemeu  12728  qredeu  12819  isprm5lem  12863  pw2dvdseu  12890  sqrt2irrap  12902  pythagtriplem2  12989  pythagtrip  13006  pclemub  13010  pcqmul  13026  pcexp  13032  pcneg  13048  pcprmpw2  13056  pcadd  13063  prmpwdvds  13078  4sqlem13m  13126  ballotfilemsf1o  13201  ennnfonelemg  13238  ennnfonelemrnh  13251  ctiunctlemfo  13274  nninfdclemf1  13287  imasival  13570  sgrppropd  13676  ismndd  13698  mndpropd  13701  mhmeql  13747  mhmmnd  13869  mulgfng  13877  issubg4m  13946  ssnmz  13964  conjnmzb  14033  gfsumval  14102  rngpropd  14194  ringpropd  14281  dvdsrtr  14346  aprlring  14538  islmod  14565  mplsubgfilemcl  14980  restbasg  15159  cnpnei  15210  cnptoprest2  15231  cnpdis  15233  lmtopcnp  15241  txcnp  15262  ismet2  15345  blininf  15415  metss2lem  15488  xmettxlem  15500  xmettx  15501  metcnp  15503  metcnpi3  15508  addcncntoplem  15552  fsumcncntop  15558  mulc1cncf  15580  cncfco  15582  mulcncf  15599  dedekindeulemuub  15608  dedekindeu  15614  dedekindicclemuub  15617  ivthinclemloc  15632  ivthinc  15634  limcimo  15656  limccnp2cntop  15668  dveflem  15717  plyf  15728  plyco  15750  plycj  15752  dvply2g  15757  logbgcd1irrap  15961  perfectlem2  15994  lgsdilem  16026  lgsquad2lem2  16081  lgsquad3  16083  2sqlem5  16118  2sqlem9  16123  usgredg4  16336  usgr1eop  16366  usgr1vr  16369  subuhgr  16393  subumgr  16395  subusgr  16396  clwwlknonex2lem2  16559  pw1map  16895  qdencn  16933  apdiff  16958  qdiff  16959