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  3099  disjiun  4054  f1imass  5866  riota5f  5947  tfrexlem  6443  tfrcl  6473  nnsucuniel  6604  nntr2  6612  pw2f1odclem  6956  fopwdom  6958  fidceq  6992  fisbth  7006  fientri3  7038  unsnfidcex  7043  undifdc  7047  iunfidisj  7074  fiuni  7106  ordiso2  7163  nninfninc  7251  acfun  7350  2omotaplemap  7404  ccfunen  7411  addcmpblnq  7515  mulcmpblnq  7516  ordpipqqs  7522  addcmpblnq0  7591  mulcmpblnq0  7592  prml  7625  addlocpr  7684  prmuloc  7714  mullocpr  7719  ltexprlemopl  7749  ltexprlemopu  7751  ltexprlemloc  7755  ltexprlemrl  7758  ltexprlemru  7760  addcanprleml  7762  addcanprlemu  7763  aptiprleml  7787  ltmprr  7790  cauappcvgprlemopl  7794  cauappcvgprlemopu  7796  cauappcvgprlemloc  7800  caucvgprlemopl  7817  caucvgprlemopu  7819  caucvgprlemloc  7823  caucvgprprlemopu  7847  caucvgprprlemloc  7851  caucvgprprlemexbt  7854  caucvgprprlemaddq  7856  suplocexprlemrl  7865  suplocexprlemdisj  7868  suplocexprlemloc  7869  suplocexprlemub  7871  addcmpblnr  7887  mulcmpblnrlemg  7888  mulcmpblnr  7889  ltsrprg  7895  mulgt0sr  7926  caucvgsrlemgt1  7943  suplocsrlemb  7954  axmulcl  8014  axcaucvglemres  8047  axpre-suploclemres  8049  axpre-suploc  8050  cnegexlem1  8282  negeu  8298  add20  8582  apreap  8695  cru  8710  apsym  8714  apcotr  8715  apadd1  8716  apneg  8719  mulext1  8720  mulge0  8727  mulap0  8762  divdivdivap  8821  prodgt0  8960  ltmul12a  8968  lt2mul2div  8987  ledivdiv  8998  lediv12a  9002  qapne  9795  xleadd1a  10030  ixxss12  10063  elfz0ubfz0  10282  qtri3or  10420  exbtwnzlemstep  10427  exbtwnzlemex  10429  exbtwnz  10430  rebtwn2zlemstep  10432  rebtwn2z  10434  btwnzge0  10480  iseqf1olemqf1o  10688  mulexpzap  10761  leexp1a  10776  hashen  10966  fihashdom  10985  hashun  10987  swrdccatin1  11216  pfxccatin12lem3  11223  pfxccat3  11225  cjap  11332  cvg1nlemres  11411  rsqrmo  11453  abslt  11514  abs3lem  11537  cau3lem  11540  rexanre  11646  xrmaxltsup  11684  climcau  11773  sumeq2  11785  summodc  11809  fisumss  11818  fsum2d  11861  fsumabs  11891  fsumiun  11903  prodeq2  11983  prodmodclem2  12003  fprodcl2lem  12031  fprodap0  12047  fprod2d  12049  fprodrec  12055  fprodap0f  12062  fprodle  12066  eirrap  12204  divalglemeunn  12347  divalglemeuneg  12349  bezoutlemnewy  12432  bezoutlemstep  12433  bezoutlemmain  12434  bezoutlembi  12441  bezoutlemeu  12443  qredeu  12534  isprm5lem  12578  pw2dvdseu  12605  sqrt2irrap  12617  pythagtriplem2  12704  pythagtrip  12721  pclemub  12725  pcqmul  12741  pcexp  12747  pcneg  12763  pcprmpw2  12771  pcadd  12778  prmpwdvds  12793  4sqlem13m  12841  ennnfonelemg  12889  ennnfonelemrnh  12902  ctiunctlemfo  12925  nninfdclemf1  12938  imasival  13253  sgrppropd  13360  ismndd  13384  mndpropd  13387  mhmeql  13439  mhmmnd  13567  mulgfng  13575  issubg4m  13644  ssnmz  13662  conjnmzb  13731  rngpropd  13832  ringpropd  13915  dvdsrtr  13978  islmod  14168  mplsubgfilemcl  14576  restbasg  14755  cnpnei  14806  cnptoprest2  14827  cnpdis  14829  lmtopcnp  14837  txcnp  14858  ismet2  14941  blininf  15011  metss2lem  15084  xmettxlem  15096  xmettx  15097  metcnp  15099  metcnpi3  15104  addcncntoplem  15148  fsumcncntop  15154  mulc1cncf  15176  cncfco  15178  mulcncf  15195  dedekindeulemuub  15204  dedekindeu  15210  dedekindicclemuub  15213  ivthinclemloc  15228  ivthinc  15230  limcimo  15252  limccnp2cntop  15264  dveflem  15313  plyf  15324  plyco  15346  plycj  15348  dvply2g  15353  logbgcd1irrap  15557  perfectlem2  15587  lgsdilem  15619  lgsquad2lem2  15674  lgsquad3  15676  2sqlem5  15711  2sqlem9  15716  2omap  16132  pw1map  16134  qdencn  16168  apdiff  16189