Theorem simpr2 988

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

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:  simplr2  1024  simprr2  1030  simp1r2  1078  simp2r2  1084  simp3r2  1090  3anandis  1325  isopolem  5723  tfrlemibacc  6223  tfrlemibfn  6225  tfr1onlembacc  6239  tfr1onlembfn  6241  tfrcllembacc  6252  tfrcllembfn  6254  prltlu  7295  prdisj  7300  prmuloc2  7375  ltntri  7890  eluzuzle  9334  xlesubadd  9666  elioc2  9719  elico2  9720  elicc2  9721  fseq1p1m1  9874  fz0fzelfz0  9904  seq3f1olemp  10275  bcval5  10509  hashdifpr  10566  summodclem2  11151  isumss2  11162  tanaddap  11446  dvds2ln  11526  divalglemeunn  11618  divalglemex  11619  divalglemeuneg  11620  isstructr  11974  restopnb  12350  icnpimaex  12380  cnptopresti  12407  psmettri  12499  isxmet2d  12517  xmettri  12541  metrtri  12546  xmetres2  12548  bldisj  12570  blss2ps  12575  blss2  12576  xmstri2  12639  mstri2  12640  xmstri  12641  mstri  12642  xmstri3  12643  mstri3  12644  msrtri  12645  comet  12668  bdbl  12672  xmetxp  12676  dvconst  12830