Theorem simplrl 503

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 474	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  rmob  2932  disjiun  3846  f1imass  5567  riota5f  5646  tfrexlem  6113  tfrcl  6143  nnsucuniel  6270  fopwdom  6606  fidceq  6639  fisbth  6653  fientri3  6679  unsnfidcex  6684  undifdc  6688  iunfidisj  6709  ordiso2  6782  addcmpblnq  6987  mulcmpblnq  6988  ordpipqqs  6994  addcmpblnq0  7063  mulcmpblnq0  7064  prml  7097  addlocpr  7156  prmuloc  7186  mullocpr  7191  ltexprlemopl  7221  ltexprlemopu  7223  ltexprlemloc  7227  ltexprlemrl  7230  ltexprlemru  7232  addcanprleml  7234  addcanprlemu  7235  aptiprleml  7259  ltmprr  7262  cauappcvgprlemopl  7266  cauappcvgprlemopu  7268  cauappcvgprlemloc  7272  caucvgprlemopl  7289  caucvgprlemopu  7291  caucvgprlemloc  7295  caucvgprprlemopu  7319  caucvgprprlemloc  7323  caucvgprprlemexbt  7326  caucvgprprlemaddq  7328  addcmpblnr  7346  mulcmpblnrlemg  7347  mulcmpblnr  7348  ltsrprg  7354  mulgt0sr  7384  caucvgsrlemgt1  7401  axmulcl  7464  axcaucvglemres  7495  cnegexlem1  7718  negeu  7734  add20  8013  apreap  8125  cru  8140  apsym  8144  apcotr  8145  apadd1  8146  apneg  8149  mulext1  8150  mulge0  8157  mulap0  8184  divdivdivap  8241  prodgt0  8374  ltmul12a  8382  lt2mul2div  8401  ledivdiv  8412  lediv12a  8416  qapne  9185  ixxss12  9385  elfz0ubfz0  9597  qtri3or  9715  exbtwnzlemstep  9720  exbtwnzlemex  9722  exbtwnz  9723  rebtwn2zlemstep  9725  rebtwn2z  9727  btwnzge0  9768  iseqf1olemqf1o  9983  mulexpzap  10056  leexp1a  10071  hashen  10253  fihashdom  10272  hashun  10274  cjap  10401  cvg1nlemres  10479  rsqrmo  10521  abslt  10582  abs3lem  10605  cau3lem  10608  rexanre  10714  climcau  10797  sumeq2  10809  isummo  10834  fisumss  10845  fsum2d  10890  fsumabs  10920  fsumiun  10932  eirrap  11126  divalglemeunn  11260  divalglemeuneg  11262  bezoutlemnewy  11324  bezoutlemstep  11325  bezoutlemmain  11326  bezoutlembi  11333  bezoutlemeu  11335  qredeu  11418  pw2dvdseu  11485  sqrt2irrap  11497  mulc1cncf  11918  cncfco  11920  qdencn  12187