Theorem simpr1 998

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

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

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 975

This theorem is referenced by:  simplr1  1034  simprr1  1040  simp1r1  1088  simp2r1  1094  simp3r1  1100  3anandis  1342  isopolem  5801  caovlem2d  6045  tfrlemibacc  6305  tfrlemibfn  6307  tfr1onlembacc  6321  tfr1onlembfn  6323  tfrcllembacc  6334  tfrcllembfn  6336  eqsupti  6973  prmuloc2  7529  ltntri  8047  elioc2  9893  elico2  9894  elicc2  9895  fseq1p1m1  10050  elfz0ubfz0  10081  ico0  10218  seq3f1olemp  10458  seq3f1oleml  10459  bcval5  10697  isumss2  11356  tanaddap  11702  dvds2ln  11786  divalglemeunn  11880  divalglemex  11881  divalglemeuneg  11882  qredeq  12050  pcdvdstr  12280  isstructr  12431  mndissubm  12697  icnpimaex  13005  cnptopresti  13032  upxp  13066  psmettri  13124  isxmet2d  13142  xmettri  13166  metrtri  13171  xmetres2  13173  bldisj  13195  blss2ps  13200  blss2  13201  xmstri2  13264  mstri2  13265  xmstri  13266  mstri  13267  xmstri3  13268  mstri3  13269  msrtri  13270  comet  13293  bdbl  13297  xmetxp  13301  dvconst  13455  findset  13980