Theorem simplrl 501

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  rmob  2906  f1imass  5434  riota5f  5512  tfrexlem  5971  fopwdom  6333  fidceq  6354  fisbth  6367  fientri3  6381  unsnfidcex  6385  ordiso2  6446  addcmpblnq  6557  mulcmpblnq  6558  ordpipqqs  6564  addcmpblnq0  6633  mulcmpblnq0  6634  prml  6667  addlocpr  6726  prmuloc  6756  mullocpr  6761  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemloc  6797  ltexprlemrl  6800  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  aptiprleml  6829  ltmprr  6832  cauappcvgprlemopl  6836  cauappcvgprlemopu  6838  cauappcvgprlemloc  6842  caucvgprlemopl  6859  caucvgprlemopu  6861  caucvgprlemloc  6865  caucvgprprlemopu  6889  caucvgprprlemloc  6893  caucvgprprlemexbt  6896  caucvgprprlemaddq  6898  addcmpblnr  6916  mulcmpblnrlemg  6917  mulcmpblnr  6918  ltsrprg  6924  mulgt0sr  6954  caucvgsrlemgt1  6971  axmulcl  7034  axcaucvglemres  7065  cnegexlem1  7283  negeu  7299  add20  7578  apreap  7687  cru  7702  apsym  7706  apcotr  7707  apadd1  7708  apneg  7711  mulext1  7712  mulge0  7719  mulap0  7744  divdivdivap  7801  prodgt0  7930  ltmul12a  7938  lt2mul2div  7957  ledivdiv  7968  lediv12a  7972  qapne  8724  ixxss12  8929  elfz0ubfz0  9136  qtri3or  9252  qbtwnzlemstep  9257  qbtwnzlemex  9259  qbtwnz  9260  rebtwn2zlemstep  9261  rebtwn2z  9263  btwnzge0  9302  expivallem  9477  mulexpzap  9516  leexp1a  9531  cjap  9793  cvg1nlemres  9871  rsqrmo  9913  abslt  9974  abs3lem  9997  cau3lem  10000  rexanre  10106  climcau  10184  divalglemeunn  10321  divalglemeuneg  10323  bezoutlemnewy  10385  bezoutlemstep  10386  bezoutlemmain  10387  bezoutlembi  10394  bezoutlemeu  10396  qredeu  10479  pw2dvdseu  10546  sqrt2irrap  10558  qdencn  10785