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  5866  tfrlemibacc  6381  tfrlemibfn  6383  tfr1onlembacc  6397  tfr1onlembfn  6399  tfrcllembacc  6410  tfrcllembfn  6412  prltlu  7549  prdisj  7554  prmuloc2  7629  ltntri  8149  eluzuzle  9603  xlesubadd  9952  elioc2  10005  elico2  10006  elicc2  10007  fseq1p1m1  10163  fz0fzelfz0  10196  seq3f1olemp  10589  bcval5  10837  hashdifpr  10894  summodclem2  11528  isumss2  11539  tanaddap  11885  dvds2ln  11970  divalglemeunn  12065  divalglemex  12066  divalglemeuneg  12067  isstructr  12636  f1ovscpbl  12898  mndissubm  13050  grpsubrcan  13156  grpsubadd  13163  grpaddsubass  13165  grpsubsub4  13168  grppnpcan2  13169  grpnpncan  13170  mulgnndir  13224  mulgnn0dir  13225  mulgdir  13227  mulgnnass  13230  mulgnn0ass  13231  mulgass  13232  mulgsubdir  13235  issubg2m  13262  eqgval  13296  qusgrp  13305  cmn32  13377  cmn12  13379  abladdsub  13388  ablsubsub23  13398  rngass  13438  srgdilem  13468  srgass  13470  ringdilem  13511  ringass  13515  opprrng  13576  opprring  13578  mulgass3  13584  unitgrp  13615  dvrass  13638  dvrdir  13642  subrgunit  13738  issubrg2  13740  aprap  13785  lsssn0  13869  islss3  13878  sralmod  13949  restopnb  14360  icnpimaex  14390  cnptopresti  14417  psmettri  14509  isxmet2d  14527  xmettri  14551  metrtri  14556  xmetres2  14558  bldisj  14580  blss2ps  14585  blss2  14586  xmstri2  14649  mstri2  14650  xmstri  14651  mstri  14652  xmstri3  14653  mstri3  14654  msrtri  14655  comet  14678  bdbl  14682  xmetxp  14686  dvconst  14873  dvconstre  14875  dvconstss  14877  gausslemma2dlem1a  15215