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  5869  tfrlemibacc  6384  tfrlemibfn  6386  tfr1onlembacc  6400  tfr1onlembfn  6402  tfrcllembacc  6413  tfrcllembfn  6415  prltlu  7554  prdisj  7559  prmuloc2  7634  ltntri  8154  eluzuzle  9609  xlesubadd  9958  elioc2  10011  elico2  10012  elicc2  10013  fseq1p1m1  10169  fz0fzelfz0  10202  seq3f1olemp  10607  bcval5  10855  hashdifpr  10912  summodclem2  11547  isumss2  11558  tanaddap  11904  dvds2ln  11989  divalglemeunn  12086  divalglemex  12087  divalglemeuneg  12088  isstructr  12693  f1ovscpbl  12955  mndissubm  13107  grpsubrcan  13213  grpsubadd  13220  grpaddsubass  13222  grpsubsub4  13225  grppnpcan2  13226  grpnpncan  13227  mulgnndir  13281  mulgnn0dir  13282  mulgdir  13284  mulgnnass  13287  mulgnn0ass  13288  mulgass  13289  mulgsubdir  13292  issubg2m  13319  eqgval  13353  qusgrp  13362  cmn32  13434  cmn12  13436  abladdsub  13445  ablsubsub23  13455  rngass  13495  srgdilem  13525  srgass  13527  ringdilem  13568  ringass  13572  opprrng  13633  opprring  13635  mulgass3  13641  unitgrp  13672  dvrass  13695  dvrdir  13699  subrgunit  13795  issubrg2  13797  aprap  13842  lsssn0  13926  islss3  13935  sralmod  14006  restopnb  14417  icnpimaex  14447  cnptopresti  14474  psmettri  14566  isxmet2d  14584  xmettri  14608  metrtri  14613  xmetres2  14615  bldisj  14637  blss2ps  14642  blss2  14643  xmstri2  14706  mstri2  14707  xmstri  14708  mstri  14709  xmstri3  14710  mstri3  14711  msrtri  14712  comet  14735  bdbl  14739  xmetxp  14743  dvconst  14930  dvconstre  14932  dvconstss  14934  sgmmul  15232  gausslemma2dlem1a  15299