Theorem simpr1 988

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

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

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 965

This theorem is referenced by:  simplr1  1024  simprr1  1030  simp1r1  1078  simp2r1  1084  simp3r1  1090  3anandis  1329  isopolem  5774  caovlem2d  6015  tfrlemibacc  6275  tfrlemibfn  6277  tfr1onlembacc  6291  tfr1onlembfn  6293  tfrcllembacc  6304  tfrcllembfn  6306  eqsupti  6942  prmuloc2  7489  ltntri  8007  elioc2  9846  elico2  9847  elicc2  9848  fseq1p1m1  10002  elfz0ubfz0  10033  ico0  10170  seq3f1olemp  10410  seq3f1oleml  10411  bcval5  10648  isumss2  11301  tanaddap  11647  dvds2ln  11731  divalglemeunn  11824  divalglemex  11825  divalglemeuneg  11826  qredeq  11988  isstructr  12275  icnpimaex  12681  cnptopresti  12708  upxp  12742  psmettri  12800  isxmet2d  12818  xmettri  12842  metrtri  12847  xmetres2  12849  bldisj  12871  blss2ps  12876  blss2  12877  xmstri2  12940  mstri2  12941  xmstri  12942  mstri  12943  xmstri3  12944  mstri3  12945  msrtri  12946  comet  12969  bdbl  12973  xmetxp  12977  dvconst  13131  findset  13591