Theorem simpr2 971

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 947

This theorem is referenced by:  simplr2  1007  simprr2  1013  simp1r2  1061  simp2r2  1067  simp3r2  1073  3anandis  1308  isopolem  5677  tfrlemibacc  6177  tfrlemibfn  6179  tfr1onlembacc  6193  tfr1onlembfn  6195  tfrcllembacc  6206  tfrcllembfn  6208  prltlu  7243  prdisj  7248  prmuloc2  7323  ltntri  7813  eluzuzle  9236  xlesubadd  9559  elioc2  9612  elico2  9613  elicc2  9614  fseq1p1m1  9767  fz0fzelfz0  9797  seq3f1olemp  10168  bcval5  10402  hashdifpr  10459  summodclem2  11043  isumss2  11054  tanaddap  11297  dvds2ln  11374  divalglemeunn  11466  divalglemex  11467  divalglemeuneg  11468  isstructr  11817  restopnb  12193  icnpimaex  12222  cnptopresti  12249  psmettri  12319  isxmet2d  12337  xmettri  12361  metrtri  12366  xmetres2  12368  bldisj  12390  blss2ps  12395  blss2  12396  xmstri2  12459  mstri2  12460  xmstri  12461  mstri  12462  xmstri3  12463  mstri3  12464  msrtri  12465  comet  12488  bdbl  12492  xmetxp  12496  dvconst  12616