Theorem simpr2 999

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

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:  simplr2  1035  simprr2  1041  simp1r2  1089  simp2r2  1095  simp3r2  1101  3anandis  1342  isopolem  5801  tfrlemibacc  6305  tfrlemibfn  6307  tfr1onlembacc  6321  tfr1onlembfn  6323  tfrcllembacc  6334  tfrcllembfn  6336  prltlu  7449  prdisj  7454  prmuloc2  7529  ltntri  8047  eluzuzle  9495  xlesubadd  9840  elioc2  9893  elico2  9894  elicc2  9895  fseq1p1m1  10050  fz0fzelfz0  10083  seq3f1olemp  10458  bcval5  10697  hashdifpr  10755  summodclem2  11345  isumss2  11356  tanaddap  11702  dvds2ln  11786  divalglemeunn  11880  divalglemex  11881  divalglemeuneg  11882  isstructr  12431  mndissubm  12697  restopnb  12975  icnpimaex  13005  cnptopresti  13032  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