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  1359  isopolem  5890  tfrlemibacc  6411  tfrlemibfn  6413  tfr1onlembacc  6427  tfr1onlembfn  6429  tfrcllembacc  6440  tfrcllembfn  6442  prltlu  7599  prdisj  7604  prmuloc2  7679  ltntri  8199  eluzuzle  9655  xlesubadd  10004  elioc2  10057  elico2  10058  elicc2  10059  fseq1p1m1  10215  fz0fzelfz0  10248  seq3f1olemp  10658  bcval5  10906  hashdifpr  10963  summodclem2  11664  isumss2  11675  tanaddap  12021  dvds2ln  12106  divalglemeunn  12203  divalglemex  12204  divalglemeuneg  12205  isstructr  12818  f1ovscpbl  13115  prdssgrpd  13218  prdsmndd  13251  mndissubm  13278  grpsubrcan  13384  grpsubadd  13391  grpaddsubass  13393  grpsubsub4  13396  grppnpcan2  13397  grpnpncan  13398  mulgnndir  13458  mulgnn0dir  13459  mulgdir  13461  mulgnnass  13464  mulgnn0ass  13465  mulgass  13466  mulgsubdir  13469  issubg2m  13496  eqgval  13530  qusgrp  13539  cmn32  13611  cmn12  13613  abladdsub  13622  ablsubsub23  13632  rngass  13672  srgdilem  13702  srgass  13704  ringdilem  13745  ringass  13749  opprrng  13810  opprring  13812  mulgass3  13818  unitgrp  13849  dvrass  13872  dvrdir  13876  subrgunit  13972  issubrg2  13974  aprap  14019  lsssn0  14103  islss3  14112  sralmod  14183  restopnb  14624  icnpimaex  14654  cnptopresti  14681  psmettri  14773  isxmet2d  14791  xmettri  14815  metrtri  14820  xmetres2  14822  bldisj  14844  blss2ps  14849  blss2  14850  xmstri2  14913  mstri2  14914  xmstri  14915  mstri  14916  xmstri3  14917  mstri3  14918  msrtri  14919  comet  14942  bdbl  14946  xmetxp  14950  dvconst  15137  dvconstre  15139  dvconstss  15141  sgmmul  15439  gausslemma2dlem1a  15506