Theorem simplrl 525

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 108	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	ad2antlr 481	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  rmob  3005  disjiun  3932  f1imass  5683  riota5f  5762  tfrexlem  6239  tfrcl  6269  nnsucuniel  6399  nntr2  6407  fopwdom  6738  fidceq  6771  fisbth  6785  fientri3  6811  unsnfidcex  6816  undifdc  6820  iunfidisj  6842  fiuni  6874  ordiso2  6928  acfun  7080  ccfunen  7096  addcmpblnq  7199  mulcmpblnq  7200  ordpipqqs  7206  addcmpblnq0  7275  mulcmpblnq0  7276  prml  7309  addlocpr  7368  prmuloc  7398  mullocpr  7403  ltexprlemopl  7433  ltexprlemopu  7435  ltexprlemloc  7439  ltexprlemrl  7442  ltexprlemru  7444  addcanprleml  7446  addcanprlemu  7447  aptiprleml  7471  ltmprr  7474  cauappcvgprlemopl  7478  cauappcvgprlemopu  7480  cauappcvgprlemloc  7484  caucvgprlemopl  7501  caucvgprlemopu  7503  caucvgprlemloc  7507  caucvgprprlemopu  7531  caucvgprprlemloc  7535  caucvgprprlemexbt  7538  caucvgprprlemaddq  7540  suplocexprlemrl  7549  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemub  7555  addcmpblnr  7571  mulcmpblnrlemg  7572  mulcmpblnr  7573  ltsrprg  7579  mulgt0sr  7610  caucvgsrlemgt1  7627  suplocsrlemb  7638  axmulcl  7698  axcaucvglemres  7731  axpre-suploclemres  7733  axpre-suploc  7734  cnegexlem1  7961  negeu  7977  add20  8260  apreap  8373  cru  8388  apsym  8392  apcotr  8393  apadd1  8394  apneg  8397  mulext1  8398  mulge0  8405  mulap0  8439  divdivdivap  8497  prodgt0  8634  ltmul12a  8642  lt2mul2div  8661  ledivdiv  8672  lediv12a  8676  qapne  9458  xleadd1a  9686  ixxss12  9719  elfz0ubfz0  9933  qtri3or  10051  exbtwnzlemstep  10056  exbtwnzlemex  10058  exbtwnz  10059  rebtwn2zlemstep  10061  rebtwn2z  10063  btwnzge0  10104  iseqf1olemqf1o  10297  mulexpzap  10364  leexp1a  10379  hashen  10562  fihashdom  10581  hashun  10583  cjap  10710  cvg1nlemres  10789  rsqrmo  10831  abslt  10892  abs3lem  10915  cau3lem  10918  rexanre  11024  xrmaxltsup  11059  climcau  11148  sumeq2  11160  summodc  11184  fisumss  11193  fsum2d  11236  fsumabs  11266  fsumiun  11278  prodeq2  11358  prodmodclem2  11378  eirrap  11520  divalglemeunn  11654  divalglemeuneg  11656  bezoutlemnewy  11720  bezoutlemstep  11721  bezoutlemmain  11722  bezoutlembi  11729  bezoutlemeu  11731  qredeu  11814  pw2dvdseu  11882  sqrt2irrap  11894  ennnfonelemg  11952  ennnfonelemrnh  11965  ctiunctlemfo  11988  restbasg  12376  cnpnei  12427  cnptoprest2  12448  cnpdis  12450  lmtopcnp  12458  txcnp  12479  ismet2  12562  blininf  12632  metss2lem  12705  xmettxlem  12717  xmettx  12718  metcnp  12720  metcnpi3  12725  addcncntoplem  12759  fsumcncntop  12764  mulc1cncf  12784  cncfco  12786  mulcncf  12799  dedekindeulemuub  12803  dedekindeu  12809  dedekindicclemuub  12812  ivthinclemloc  12827  ivthinc  12829  limcimo  12842  limccnp2cntop  12854  dveflem  12895  logbgcd1irrap  13095  qdencn  13397  apdiff  13416