Theorem simpr2 1030

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

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

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 1006

This theorem is referenced by:  simplr2  1066  simprr2  1072  simp1r2  1120  simp2r2  1126  simp3r2  1132  3anandis  1383  isopolem  5963  tfrlemibacc  6492  tfrlemibfn  6494  tfr1onlembacc  6508  tfr1onlembfn  6510  tfrcllembacc  6521  tfrcllembfn  6523  prltlu  7707  prdisj  7712  prmuloc2  7787  ltntri  8307  eluzuzle  9764  xlesubadd  10118  elioc2  10171  elico2  10172  elicc2  10173  fseq1p1m1  10329  fz0fzelfz0  10362  seq3f1olemp  10778  bcval5  11026  hashdifpr  11085  hashtpgim  11110  swrdsbslen  11251  ccatswrd  11255  swrdswrdlem  11289  summodclem2  11961  isumss2  11972  tanaddap  12318  dvds2ln  12403  divalglemeunn  12500  divalglemex  12501  divalglemeuneg  12502  isstructr  13115  f1ovscpbl  13413  prdssgrpd  13516  prdsmndd  13549  mndissubm  13576  grpsubrcan  13682  grpsubadd  13689  grpaddsubass  13691  grpsubsub4  13694  grppnpcan2  13695  grpnpncan  13696  mulgnndir  13756  mulgnn0dir  13757  mulgdir  13759  mulgnnass  13762  mulgnn0ass  13763  mulgass  13764  mulgsubdir  13767  issubg2m  13794  eqgval  13828  qusgrp  13837  cmn32  13909  cmn12  13911  abladdsub  13920  ablsubsub23  13930  rngass  13971  srgdilem  14001  srgass  14003  ringdilem  14044  ringass  14048  opprrng  14109  opprring  14111  mulgass3  14117  unitgrp  14149  dvrass  14172  dvrdir  14176  subrgunit  14272  issubrg2  14274  aprap  14319  lsssn0  14403  islss3  14412  sralmod  14483  restopnb  14924  icnpimaex  14954  cnptopresti  14981  psmettri  15073  isxmet2d  15091  xmettri  15115  metrtri  15120  xmetres2  15122  bldisj  15144  blss2ps  15149  blss2  15150  xmstri2  15213  mstri2  15214  xmstri  15215  mstri  15216  xmstri3  15217  mstri3  15218  msrtri  15219  comet  15242  bdbl  15246  xmetxp  15250  dvconst  15437  dvconstre  15439  dvconstss  15441  sgmmul  15739  gausslemma2dlem1a  15806  pw1ndom3  16640