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  6001  tfrlemibacc  6570  tfrlemibfn  6572  tfr1onlembacc  6586  tfr1onlembfn  6588  tfrcllembacc  6599  tfrcllembfn  6601  prltlu  7818  prdisj  7823  prmuloc2  7898  ltntri  8417  eluzuzle  9880  xlesubadd  10235  elioc2  10288  elico2  10289  elicc2  10290  fseq1p1m1  10450  fz0fzelfz0  10483  seq3f1olemp  10901  bcval5  11150  hashdifpr  11210  hashtpgim  11242  swrdsbslen  11383  ccatswrd  11387  swrdswrdlem  11421  summodclem2  12093  isumss2  12104  tanaddap  12450  dvds2ln  12535  divalglemeunn  12632  divalglemex  12633  divalglemeuneg  12634  isstructr  13311  f1ovscpbl  13576  mndissubm  13730  grpsubrcan  13836  grpsubadd  13843  grpaddsubass  13845  grpsubsub4  13848  grppnpcan2  13849  grpnpncan  13850  mulgnndir  13904  mulgnn0dir  13905  mulgdir  13907  mulgnnass  13910  mulgnn0ass  13911  mulgass  13912  mulgsubdir  13915  issubg2m  13942  eqgval  13976  qusgrp  13985  cmn32  14057  cmn12  14059  abladdsub  14068  ablsubsub23  14078  prdssgrpd  14133  prdsmndd  14136  rngass  14178  srgdilem  14212  srgass  14214  ringdilem  14255  ringass  14259  opprrng  14320  opprring  14322  mulgass3  14329  unitgrp  14361  dvrass  14384  dvrdir  14388  subrgunit  14485  issubrg2  14487  aprap  14536  lsssn0  14644  islss3  14653  sralmod  14724  restopnb  15172  icnpimaex  15202  cnptopresti  15229  psmettri  15321  isxmet2d  15339  xmettri  15363  metrtri  15368  xmetres2  15370  bldisj  15392  blss2ps  15397  blss2  15398  xmstri2  15461  mstri2  15462  xmstri  15463  mstri  15464  xmstri3  15465  mstri3  15466  msrtri  15467  comet  15490  bdbl  15494  xmetxp  15498  dvconst  15685  dvconstre  15687  dvconstss  15689  sgmmul  15990  gausslemma2dlem1a  16057  pw1ndom3  16890