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  5844  tfrlemibacc  6351  tfrlemibfn  6353  tfr1onlembacc  6367  tfr1onlembfn  6369  tfrcllembacc  6380  tfrcllembfn  6382  prltlu  7516  prdisj  7521  prmuloc2  7596  ltntri  8115  eluzuzle  9566  xlesubadd  9913  elioc2  9966  elico2  9967  elicc2  9968  fseq1p1m1  10124  fz0fzelfz0  10157  seq3f1olemp  10533  bcval5  10775  hashdifpr  10832  summodclem2  11422  isumss2  11433  tanaddap  11779  dvds2ln  11863  divalglemeunn  11958  divalglemex  11959  divalglemeuneg  11960  isstructr  12527  f1ovscpbl  12789  mndissubm  12927  grpsubrcan  13025  grpsubadd  13032  grpaddsubass  13034  grpsubsub4  13037  grppnpcan2  13038  grpnpncan  13039  mulgnndir  13091  mulgnn0dir  13092  mulgdir  13094  mulgnnass  13097  mulgnn0ass  13098  mulgass  13099  mulgsubdir  13102  issubg2m  13128  eqgval  13162  qusgrp  13171  cmn32  13243  cmn12  13245  abladdsub  13254  ablsubsub23  13264  rngass  13293  srgdilem  13323  srgass  13325  ringdilem  13366  ringass  13370  opprrng  13427  opprring  13429  mulgass3  13435  unitgrp  13466  dvrass  13489  dvrdir  13493  subrgunit  13586  issubrg2  13588  aprap  13602  lsssn0  13686  islss3  13695  sralmod  13766  restopnb  14141  icnpimaex  14171  cnptopresti  14198  psmettri  14290  isxmet2d  14308  xmettri  14332  metrtri  14337  xmetres2  14339  bldisj  14361  blss2ps  14366  blss2  14367  xmstri2  14430  mstri2  14431  xmstri  14432  mstri  14433  xmstri3  14434  mstri3  14435  msrtri  14436  comet  14459  bdbl  14463  xmetxp  14467  dvconst  14621