Theorem simpr1 910

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

Syntax hints:   -> wi 4   /\ wa 97   /\ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  simplr1  946  simprr1  952  simp1r1  1000  simp2r1  1006  simp3r1  1012  3anandis  1237  isopolem  5461  caovlem2d  5693  tfrlemibacc  5940  tfrlemibfn  5942  prmuloc2  6665  elioc2  8805  elico2  8806  elicc2  8807  fseq1p1m1  8956  elfz0ubfz0  8982  findset  10070