Theorem simpr2 989

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

Assertion

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

Proof of Theorem simpr2

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

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:  simplr2  1025  simprr2  1031  simp1r2  1079  simp2r2  1085  simp3r2  1091  3anandis  1326  isopolem  5763  tfrlemibacc  6263  tfrlemibfn  6265  tfr1onlembacc  6279  tfr1onlembfn  6281  tfrcllembacc  6292  tfrcllembfn  6294  prltlu  7386  prdisj  7391  prmuloc2  7466  ltntri  7982  eluzuzle  9426  xlesubadd  9765  elioc2  9818  elico2  9819  elicc2  9820  fseq1p1m1  9974  fz0fzelfz0  10004  seq3f1olemp  10379  bcval5  10614  hashdifpr  10671  summodclem2  11256  isumss2  11267  tanaddap  11613  dvds2ln  11693  divalglemeunn  11785  divalglemex  11786  divalglemeuneg  11787  isstructr  12144  restopnb  12520  icnpimaex  12550  cnptopresti  12577  psmettri  12669  isxmet2d  12687  xmettri  12711  metrtri  12716  xmetres2  12718  bldisj  12740  blss2ps  12745  blss2  12746  xmstri2  12809  mstri2  12810  xmstri  12811  mstri  12812  xmstri3  12813  mstri3  12814  msrtri  12815  comet  12838  bdbl  12842  xmetxp  12846  dvconst  13000