Theorem simpr2 1031

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

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

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 1007

This theorem is referenced by:  simplr2  1067  simprr2  1073  simp1r2  1121  simp2r2  1127  simp3r2  1133  3anandis  1384  isopolem  5995  tfrlemibacc  6557  tfrlemibfn  6559  tfr1onlembacc  6573  tfr1onlembfn  6575  tfrcllembacc  6586  tfrcllembfn  6588  prltlu  7802  prdisj  7807  prmuloc2  7882  ltntri  8401  eluzuzle  9862  xlesubadd  10216  elioc2  10269  elico2  10270  elicc2  10271  fseq1p1m1  10428  fz0fzelfz0  10461  seq3f1olemp  10877  bcval5  11125  hashdifpr  11185  hashtpgim  11217  swrdsbslen  11358  ccatswrd  11362  swrdswrdlem  11396  summodclem2  12068  isumss2  12079  tanaddap  12425  dvds2ln  12510  divalglemeunn  12607  divalglemex  12608  divalglemeuneg  12609  isstructr  13227  f1ovscpbl  13525  prdssgrpd  13628  prdsmndd  13661  mndissubm  13688  grpsubrcan  13794  grpsubadd  13801  grpaddsubass  13803  grpsubsub4  13806  grppnpcan2  13807  grpnpncan  13808  mulgnndir  13868  mulgnn0dir  13869  mulgdir  13871  mulgnnass  13874  mulgnn0ass  13875  mulgass  13876  mulgsubdir  13879  issubg2m  13906  eqgval  13940  qusgrp  13949  cmn32  14021  cmn12  14023  abladdsub  14032  ablsubsub23  14042  rngass  14083  srgdilem  14113  srgass  14115  ringdilem  14156  ringass  14160  opprrng  14221  opprring  14223  mulgass3  14229  unitgrp  14261  dvrass  14284  dvrdir  14288  subrgunit  14384  issubrg2  14386  aprap  14432  lsssn0  14518  islss3  14527  sralmod  14598  restopnb  15046  icnpimaex  15076  cnptopresti  15103  psmettri  15195  isxmet2d  15213  xmettri  15237  metrtri  15242  xmetres2  15244  bldisj  15266  blss2ps  15271  blss2  15272  xmstri2  15335  mstri2  15336  xmstri  15337  mstri  15338  xmstri3  15339  mstri3  15340  msrtri  15341  comet  15364  bdbl  15368  xmetxp  15372  dvconst  15559  dvconstre  15561  dvconstss  15563  sgmmul  15864  gausslemma2dlem1a  15931  pw1ndom3  16764