Theorem simpr2 1006

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simplr2  1042  simprr2  1048  simp1r2  1096  simp2r2  1102  simp3r2  1108  3anandis  1358  isopolem  5865  tfrlemibacc  6379  tfrlemibfn  6381  tfr1onlembacc  6395  tfr1onlembfn  6397  tfrcllembacc  6408  tfrcllembfn  6410  prltlu  7547  prdisj  7552  prmuloc2  7627  ltntri  8147  eluzuzle  9600  xlesubadd  9949  elioc2  10002  elico2  10003  elicc2  10004  fseq1p1m1  10160  fz0fzelfz0  10193  seq3f1olemp  10586  bcval5  10834  hashdifpr  10891  summodclem2  11525  isumss2  11536  tanaddap  11882  dvds2ln  11967  divalglemeunn  12062  divalglemex  12063  divalglemeuneg  12064  isstructr  12633  f1ovscpbl  12895  mndissubm  13047  grpsubrcan  13153  grpsubadd  13160  grpaddsubass  13162  grpsubsub4  13165  grppnpcan2  13166  grpnpncan  13167  mulgnndir  13221  mulgnn0dir  13222  mulgdir  13224  mulgnnass  13227  mulgnn0ass  13228  mulgass  13229  mulgsubdir  13232  issubg2m  13259  eqgval  13293  qusgrp  13302  cmn32  13374  cmn12  13376  abladdsub  13385  ablsubsub23  13395  rngass  13435  srgdilem  13465  srgass  13467  ringdilem  13508  ringass  13512  opprrng  13573  opprring  13575  mulgass3  13581  unitgrp  13612  dvrass  13635  dvrdir  13639  subrgunit  13735  issubrg2  13737  aprap  13782  lsssn0  13866  islss3  13875  sralmod  13946  restopnb  14349  icnpimaex  14379  cnptopresti  14406  psmettri  14498  isxmet2d  14516  xmettri  14540  metrtri  14545  xmetres2  14547  bldisj  14569  blss2ps  14574  blss2  14575  xmstri2  14638  mstri2  14639  xmstri  14640  mstri  14641  xmstri3  14642  mstri3  14643  msrtri  14644  comet  14667  bdbl  14671  xmetxp  14675  dvconst  14846  gausslemma2dlem1a  15174