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  5872  tfrlemibacc  6393  tfrlemibfn  6395  tfr1onlembacc  6409  tfr1onlembfn  6411  tfrcllembacc  6422  tfrcllembfn  6424  prltlu  7573  prdisj  7578  prmuloc2  7653  ltntri  8173  eluzuzle  9628  xlesubadd  9977  elioc2  10030  elico2  10031  elicc2  10032  fseq1p1m1  10188  fz0fzelfz0  10221  seq3f1olemp  10626  bcval5  10874  hashdifpr  10931  summodclem2  11566  isumss2  11577  tanaddap  11923  dvds2ln  12008  divalglemeunn  12105  divalglemex  12106  divalglemeuneg  12107  isstructr  12720  f1ovscpbl  13016  prdssgrpd  13119  prdsmndd  13152  mndissubm  13179  grpsubrcan  13285  grpsubadd  13292  grpaddsubass  13294  grpsubsub4  13297  grppnpcan2  13298  grpnpncan  13299  mulgnndir  13359  mulgnn0dir  13360  mulgdir  13362  mulgnnass  13365  mulgnn0ass  13366  mulgass  13367  mulgsubdir  13370  issubg2m  13397  eqgval  13431  qusgrp  13440  cmn32  13512  cmn12  13514  abladdsub  13523  ablsubsub23  13533  rngass  13573  srgdilem  13603  srgass  13605  ringdilem  13646  ringass  13650  opprrng  13711  opprring  13713  mulgass3  13719  unitgrp  13750  dvrass  13773  dvrdir  13777  subrgunit  13873  issubrg2  13875  aprap  13920  lsssn0  14004  islss3  14013  sralmod  14084  restopnb  14525  icnpimaex  14555  cnptopresti  14582  psmettri  14674  isxmet2d  14692  xmettri  14716  metrtri  14721  xmetres2  14723  bldisj  14745  blss2ps  14750  blss2  14751  xmstri2  14814  mstri2  14815  xmstri  14816  mstri  14817  xmstri3  14818  mstri3  14819  msrtri  14820  comet  14843  bdbl  14847  xmetxp  14851  dvconst  15038  dvconstre  15040  dvconstss  15042  sgmmul  15340  gausslemma2dlem1a  15407