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  5973  tfrlemibacc  6535  tfrlemibfn  6537  tfr1onlembacc  6551  tfr1onlembfn  6553  tfrcllembacc  6564  tfrcllembfn  6566  prltlu  7750  prdisj  7755  prmuloc2  7830  ltntri  8349  eluzuzle  9808  xlesubadd  10162  elioc2  10215  elico2  10216  elicc2  10217  fseq1p1m1  10374  fz0fzelfz0  10407  seq3f1olemp  10823  bcval5  11071  hashdifpr  11130  hashtpgim  11155  swrdsbslen  11296  ccatswrd  11300  swrdswrdlem  11334  summodclem2  12006  isumss2  12017  tanaddap  12363  dvds2ln  12448  divalglemeunn  12545  divalglemex  12546  divalglemeuneg  12547  isstructr  13160  f1ovscpbl  13458  prdssgrpd  13561  prdsmndd  13594  mndissubm  13621  grpsubrcan  13727  grpsubadd  13734  grpaddsubass  13736  grpsubsub4  13739  grppnpcan2  13740  grpnpncan  13741  mulgnndir  13801  mulgnn0dir  13802  mulgdir  13804  mulgnnass  13807  mulgnn0ass  13808  mulgass  13809  mulgsubdir  13812  issubg2m  13839  eqgval  13873  qusgrp  13882  cmn32  13954  cmn12  13956  abladdsub  13965  ablsubsub23  13975  rngass  14016  srgdilem  14046  srgass  14048  ringdilem  14089  ringass  14093  opprrng  14154  opprring  14156  mulgass3  14162  unitgrp  14194  dvrass  14217  dvrdir  14221  subrgunit  14317  issubrg2  14319  aprap  14365  lsssn0  14449  islss3  14458  sralmod  14529  restopnb  14975  icnpimaex  15005  cnptopresti  15032  psmettri  15124  isxmet2d  15142  xmettri  15166  metrtri  15171  xmetres2  15173  bldisj  15195  blss2ps  15200  blss2  15201  xmstri2  15264  mstri2  15265  xmstri  15266  mstri  15267  xmstri3  15268  mstri3  15269  msrtri  15270  comet  15293  bdbl  15297  xmetxp  15301  dvconst  15488  dvconstre  15490  dvconstss  15492  sgmmul  15793  gausslemma2dlem1a  15860  pw1ndom3  16693