Theorem simpr1 987

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpr1	|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ps )

Proof of Theorem simpr1

Step	Hyp	Ref	Expression
1		simp1 981	. 2 |- ( ( ps /\ ch /\ th ) -> ps )
2	1	adantl 275	1 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 962

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 depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  simplr1  1023  simprr1  1029  simp1r1  1077  simp2r1  1083  simp3r1  1089  3anandis  1325  isopolem  5716  caovlem2d  5956  tfrlemibacc  6216  tfrlemibfn  6218  tfr1onlembacc  6232  tfr1onlembfn  6234  tfrcllembacc  6245  tfrcllembfn  6247  eqsupti  6876  prmuloc2  7368  ltntri  7883  elioc2  9712  elico2  9713  elicc2  9714  fseq1p1m1  9867  elfz0ubfz0  9895  ico0  10032  seq3f1olemp  10268  seq3f1oleml  10269  bcval5  10502  isumss2  11155  tanaddap  11435  dvds2ln  11515  divalglemeunn  11607  divalglemex  11608  divalglemeuneg  11609  qredeq  11766  isstructr  11963  icnpimaex  12369  cnptopresti  12396  upxp  12430  psmettri  12488  isxmet2d  12506  xmettri  12530  metrtri  12535  xmetres2  12537  bldisj  12559  blss2ps  12564  blss2  12565  xmstri2  12628  mstri2  12629  xmstri  12630  mstri  12631  xmstri3  12632  mstri3  12633  msrtri  12634  comet  12657  bdbl  12661  xmetxp  12665  dvconst  12819  findset  13132