Theorem simpr1 949

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 943	. 2 |- ( ( ps /\ ch /\ th ) -> ps )
2	1	adantl 271	1 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 924

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

This theorem is referenced by:  simplr1  985  simprr1  991  simp1r1  1039  simp2r1  1045  simp3r1  1051  3anandis  1283  isopolem  5593  caovlem2d  5829  tfrlemibacc  6083  tfrlemibfn  6085  tfr1onlembacc  6099  tfr1onlembfn  6101  tfrcllembacc  6112  tfrcllembfn  6114  eqsupti  6681  prmuloc2  7116  elioc2  9344  elico2  9345  elicc2  9346  fseq1p1m1  9496  elfz0ubfz0  9524  ico0  9661  seq3f1olemp  9919  seq3f1oleml  9920  ibcval5  10159  isumss2  10772  tanaddap  11017  dvds2ln  11094  divalglemeunn  11186  divalglemex  11187  divalglemeuneg  11188  qredeq  11343  findset  11723