Theorem simpr2 994

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

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

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 970

This theorem is referenced by:  simplr2  1030  simprr2  1036  simp1r2  1084  simp2r2  1090  simp3r2  1096  3anandis  1337  isopolem  5790  tfrlemibacc  6294  tfrlemibfn  6296  tfr1onlembacc  6310  tfr1onlembfn  6312  tfrcllembacc  6323  tfrcllembfn  6325  prltlu  7428  prdisj  7433  prmuloc2  7508  ltntri  8026  eluzuzle  9474  xlesubadd  9819  elioc2  9872  elico2  9873  elicc2  9874  fseq1p1m1  10029  fz0fzelfz0  10062  seq3f1olemp  10437  bcval5  10676  hashdifpr  10733  summodclem2  11323  isumss2  11334  tanaddap  11680  dvds2ln  11764  divalglemeunn  11858  divalglemex  11859  divalglemeuneg  11860  isstructr  12409  restopnb  12821  icnpimaex  12851  cnptopresti  12878  psmettri  12970  isxmet2d  12988  xmettri  13012  metrtri  13017  xmetres2  13019  bldisj  13041  blss2ps  13046  blss2  13047  xmstri2  13110  mstri2  13111  xmstri  13112  mstri  13113  xmstri3  13114  mstri3  13115  msrtri  13116  comet  13139  bdbl  13143  xmetxp  13147  dvconst  13301