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  3125  disjiun  4083  f1imass  5914  riota5f  5997  tfrexlem  6499  tfrcl  6529  nnsucuniel  6662  nntr2  6670  pw2f1odclem  7019  fopwdom  7021  fidceq  7055  fisbth  7071  fidcen  7087  fientri3  7106  unsnfidcex  7111  undifdc  7115  iunfidisj  7144  fiuni  7176  ordiso2  7233  nninfninc  7321  acfun  7421  2omotaplemap  7475  ccfunen  7482  addcmpblnq  7586  mulcmpblnq  7587  ordpipqqs  7593  addcmpblnq0  7662  mulcmpblnq0  7663  prml  7696  addlocpr  7755  prmuloc  7785  mullocpr  7790  ltexprlemopl  7820  ltexprlemopu  7822  ltexprlemloc  7826  ltexprlemrl  7829  ltexprlemru  7831  addcanprleml  7833  addcanprlemu  7834  aptiprleml  7858  ltmprr  7861  cauappcvgprlemopl  7865  cauappcvgprlemopu  7867  cauappcvgprlemloc  7871  caucvgprlemopl  7888  caucvgprlemopu  7890  caucvgprlemloc  7894  caucvgprprlemopu  7918  caucvgprprlemloc  7922  caucvgprprlemexbt  7925  caucvgprprlemaddq  7927  suplocexprlemrl  7936  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemub  7942  addcmpblnr  7958  mulcmpblnrlemg  7959  mulcmpblnr  7960  ltsrprg  7966  mulgt0sr  7997  caucvgsrlemgt1  8014  suplocsrlemb  8025  axmulcl  8085  axcaucvglemres  8118  axpre-suploclemres  8120  axpre-suploc  8121  cnegexlem1  8353  negeu  8369  add20  8653  apreap  8766  cru  8781  apsym  8785  apcotr  8786  apadd1  8787  apneg  8790  mulext1  8791  mulge0  8798  mulap0  8833  divdivdivap  8892  prodgt0  9031  ltmul12a  9039  lt2mul2div  9058  ledivdiv  9069  lediv12a  9073  qapne  9872  xleadd1a  10107  ixxss12  10140  elfz0ubfz0  10359  qtri3or  10499  exbtwnzlemstep  10506  exbtwnzlemex  10508  exbtwnz  10509  rebtwn2zlemstep  10511  rebtwn2z  10513  btwnzge0  10559  iseqf1olemqf1o  10767  mulexpzap  10840  leexp1a  10855  hashen  11045  fihashdom  11065  hashun  11067  swrdccatin1  11305  pfxccatin12lem3  11312  pfxccat3  11314  cjap  11466  cvg1nlemres  11545  rsqrmo  11587  abslt  11648  abs3lem  11671  cau3lem  11674  rexanre  11780  xrmaxltsup  11818  climcau  11907  sumeq2  11919  summodc  11943  fisumss  11952  fsum2d  11995  fsumabs  12025  fsumiun  12037  prodeq2  12117  prodmodclem2  12137  fprodcl2lem  12165  fprodap0  12181  fprod2d  12183  fprodrec  12189  fprodap0f  12196  fprodle  12200  eirrap  12338  divalglemeunn  12481  divalglemeuneg  12483  bezoutlemnewy  12566  bezoutlemstep  12567  bezoutlemmain  12568  bezoutlembi  12575  bezoutlemeu  12577  qredeu  12668  isprm5lem  12712  pw2dvdseu  12739  sqrt2irrap  12751  pythagtriplem2  12838  pythagtrip  12855  pclemub  12859  pcqmul  12875  pcexp  12881  pcneg  12897  pcprmpw2  12905  pcadd  12912  prmpwdvds  12927  4sqlem13m  12975  ennnfonelemg  13023  ennnfonelemrnh  13036  ctiunctlemfo  13059  nninfdclemf1  13072  imasival  13388  sgrppropd  13495  ismndd  13519  mndpropd  13522  mhmeql  13574  mhmmnd  13702  mulgfng  13710  issubg4m  13779  ssnmz  13797  conjnmzb  13866  rngpropd  13967  ringpropd  14050  dvdsrtr  14114  islmod  14304  mplsubgfilemcl  14712  restbasg  14891  cnpnei  14942  cnptoprest2  14963  cnpdis  14965  lmtopcnp  14973  txcnp  14994  ismet2  15077  blininf  15147  metss2lem  15220  xmettxlem  15232  xmettx  15233  metcnp  15235  metcnpi3  15240  addcncntoplem  15284  fsumcncntop  15290  mulc1cncf  15312  cncfco  15314  mulcncf  15331  dedekindeulemuub  15340  dedekindeu  15346  dedekindicclemuub  15349  ivthinclemloc  15364  ivthinc  15366  limcimo  15388  limccnp2cntop  15400  dveflem  15449  plyf  15460  plyco  15482  plycj  15484  dvply2g  15489  logbgcd1irrap  15693  perfectlem2  15723  lgsdilem  15755  lgsquad2lem2  15810  lgsquad3  15812  2sqlem5  15847  2sqlem9  15852  usgredg4  16065  usgr1eop  16095  usgr1vr  16098  subuhgr  16122  subumgr  16124  subusgr  16125  clwwlknonex2lem2  16288  2omap  16594  pw1map  16596  qdencn  16631  apdiff  16652  gfsumval  16680