Theorem simpr3 989

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

Assertion

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

Proof of Theorem simpr3

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

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

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 964

This theorem is referenced by:  simplr3  1025  simprr3  1031  simp1r3  1079  simp2r3  1085  simp3r3  1091  3anandis  1325  isopolem  5716  tfrlemibacc  6216  tfrlemibxssdm  6217  tfrlemibfn  6218  tfr1onlembacc  6232  tfr1onlembxssdm  6233  tfr1onlembfn  6234  tfrcllembacc  6245  tfrcllembxssdm  6246  tfrcllembfn  6247  elfir  6854  prloc  7292  prmuloc2  7368  ltntri  7883  eluzuzle  9327  xlesubadd  9659  elioc2  9712  elico2  9713  elicc2  9714  fseq1p1m1  9867  seq3f1olemp  10268  seq3f1oleml  10269  bcval5  10502  hashdifpr  10559  isumss2  11155  tanaddap  11435  dvds2ln  11515  divalglemeunn  11607  divalglemex  11608  divalglemeuneg  11609  restopnb  12339  icnpimaex  12369  cnptopresti  12396  psmettri  12488  isxmet2d  12506  xmettri  12530  metrtri  12535  xmetres2  12537  bldisj  12559  blss2ps  12564  blss2  12565  xmstri2  12628  mstri2  12629  xmstri  12630  mstri  12631  xmstri3  12632  mstri3  12633  msrtri  12634  comet  12657  bdbl  12661  xmetxp  12665  dvconst  12819