Theorem simpr2 1004

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

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

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 980

This theorem is referenced by:  simplr2  1040  simprr2  1046  simp1r2  1094  simp2r2  1100  simp3r2  1106  3anandis  1347  isopolem  5823  tfrlemibacc  6327  tfrlemibfn  6329  tfr1onlembacc  6343  tfr1onlembfn  6345  tfrcllembacc  6356  tfrcllembfn  6358  prltlu  7486  prdisj  7491  prmuloc2  7566  ltntri  8085  eluzuzle  9536  xlesubadd  9883  elioc2  9936  elico2  9937  elicc2  9938  fseq1p1m1  10094  fz0fzelfz0  10127  seq3f1olemp  10502  bcval5  10743  hashdifpr  10800  summodclem2  11390  isumss2  11401  tanaddap  11747  dvds2ln  11831  divalglemeunn  11926  divalglemex  11927  divalglemeuneg  11928  isstructr  12477  f1ovscpbl  12733  mndissubm  12866  grpsubrcan  12951  grpsubadd  12958  grpaddsubass  12960  grpsubsub4  12963  grppnpcan2  12964  grpnpncan  12965  mulgnndir  13012  mulgnn0dir  13013  mulgdir  13015  mulgnnass  13018  mulgnn0ass  13019  mulgass  13020  mulgsubdir  13023  issubg2m  13049  eqgval  13082  cmn32  13107  cmn12  13109  abladdsub  13118  ablsubsub23  13128  srgdilem  13152  srgass  13154  ringdilem  13195  ringass  13199  opprring  13249  mulgass3  13254  unitgrp  13285  dvrass  13308  dvrdir  13312  subrgunit  13360  issubrg2  13362  aprap  13376  restopnb  13684  icnpimaex  13714  cnptopresti  13741  psmettri  13833  isxmet2d  13851  xmettri  13875  metrtri  13880  xmetres2  13882  bldisj  13904  blss2ps  13909  blss2  13910  xmstri2  13973  mstri2  13974  xmstri  13975  mstri  13976  xmstri3  13977  mstri3  13978  msrtri  13979  comet  14002  bdbl  14006  xmetxp  14010  dvconst  14164