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  5914  tfrlemibacc  6435  tfrlemibfn  6437  tfr1onlembacc  6451  tfr1onlembfn  6453  tfrcllembacc  6464  tfrcllembfn  6466  prltlu  7635  prdisj  7640  prmuloc2  7715  ltntri  8235  eluzuzle  9691  xlesubadd  10040  elioc2  10093  elico2  10094  elicc2  10095  fseq1p1m1  10251  fz0fzelfz0  10284  seq3f1olemp  10697  bcval5  10945  hashdifpr  11002  swrdsbslen  11157  ccatswrd  11161  swrdswrdlem  11195  summodclem2  11808  isumss2  11819  tanaddap  12165  dvds2ln  12250  divalglemeunn  12347  divalglemex  12348  divalglemeuneg  12349  isstructr  12962  f1ovscpbl  13259  prdssgrpd  13362  prdsmndd  13395  mndissubm  13422  grpsubrcan  13528  grpsubadd  13535  grpaddsubass  13537  grpsubsub4  13540  grppnpcan2  13541  grpnpncan  13542  mulgnndir  13602  mulgnn0dir  13603  mulgdir  13605  mulgnnass  13608  mulgnn0ass  13609  mulgass  13610  mulgsubdir  13613  issubg2m  13640  eqgval  13674  qusgrp  13683  cmn32  13755  cmn12  13757  abladdsub  13766  ablsubsub23  13776  rngass  13816  srgdilem  13846  srgass  13848  ringdilem  13889  ringass  13893  opprrng  13954  opprring  13956  mulgass3  13962  unitgrp  13993  dvrass  14016  dvrdir  14020  subrgunit  14116  issubrg2  14118  aprap  14163  lsssn0  14247  islss3  14256  sralmod  14327  restopnb  14768  icnpimaex  14798  cnptopresti  14825  psmettri  14917  isxmet2d  14935  xmettri  14959  metrtri  14964  xmetres2  14966  bldisj  14988  blss2ps  14993  blss2  14994  xmstri2  15057  mstri2  15058  xmstri  15059  mstri  15060  xmstri3  15061  mstri3  15062  msrtri  15063  comet  15086  bdbl  15090  xmetxp  15094  dvconst  15281  dvconstre  15283  dvconstss  15285  sgmmul  15583  gausslemma2dlem1a  15650