Theorem simpr2 1007

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

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

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 983

This theorem is referenced by:  simplr2  1043  simprr2  1049  simp1r2  1097  simp2r2  1103  simp3r2  1109  3anandis  1360  isopolem  5904  tfrlemibacc  6425  tfrlemibfn  6427  tfr1onlembacc  6441  tfr1onlembfn  6443  tfrcllembacc  6454  tfrcllembfn  6456  prltlu  7620  prdisj  7625  prmuloc2  7700  ltntri  8220  eluzuzle  9676  xlesubadd  10025  elioc2  10078  elico2  10079  elicc2  10080  fseq1p1m1  10236  fz0fzelfz0  10269  seq3f1olemp  10682  bcval5  10930  hashdifpr  10987  swrdsbslen  11142  ccatswrd  11146  swrdswrdlem  11180  summodclem2  11768  isumss2  11779  tanaddap  12125  dvds2ln  12210  divalglemeunn  12307  divalglemex  12308  divalglemeuneg  12309  isstructr  12922  f1ovscpbl  13219  prdssgrpd  13322  prdsmndd  13355  mndissubm  13382  grpsubrcan  13488  grpsubadd  13495  grpaddsubass  13497  grpsubsub4  13500  grppnpcan2  13501  grpnpncan  13502  mulgnndir  13562  mulgnn0dir  13563  mulgdir  13565  mulgnnass  13568  mulgnn0ass  13569  mulgass  13570  mulgsubdir  13573  issubg2m  13600  eqgval  13634  qusgrp  13643  cmn32  13715  cmn12  13717  abladdsub  13726  ablsubsub23  13736  rngass  13776  srgdilem  13806  srgass  13808  ringdilem  13849  ringass  13853  opprrng  13914  opprring  13916  mulgass3  13922  unitgrp  13953  dvrass  13976  dvrdir  13980  subrgunit  14076  issubrg2  14078  aprap  14123  lsssn0  14207  islss3  14216  sralmod  14287  restopnb  14728  icnpimaex  14758  cnptopresti  14785  psmettri  14877  isxmet2d  14895  xmettri  14919  metrtri  14924  xmetres2  14926  bldisj  14948  blss2ps  14953  blss2  14954  xmstri2  15017  mstri2  15018  xmstri  15019  mstri  15020  xmstri3  15021  mstri3  15022  msrtri  15023  comet  15046  bdbl  15050  xmetxp  15054  dvconst  15241  dvconstre  15243  dvconstss  15245  sgmmul  15543  gausslemma2dlem1a  15610