Theorem simpr2 1035

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simplr2  1071  simprr2  1077  simp1r2  1125  simp2r2  1131  simp3r2  1137  3anandis  1388  isopolem  6028  tfrlemibacc  6597  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembfn  6628  prltlu  7854  prdisj  7859  prmuloc2  7934  ltntri  8454  eluzuzle  9930  xlesubadd  10285  elioc2  10338  elico2  10339  elicc2  10340  fseq1p1m1  10501  fz0fzelfz0  10534  seq3f1olemp  10952  bcval5  11201  hashdifpr  11261  hashtpgim  11297  swrdsbslen  11438  ccatswrd  11442  swrdswrdlem  11476  summodclem2  12149  isumss2  12160  tanaddap  12506  dvds2ln  12591  divalglemeunn  12688  divalglemex  12689  divalglemeuneg  12690  isstructr  13367  f1ovscpbl  13633  mndissubm  13782  grpsubrcan  13886  grpsubadd  13893  grpaddsubass  13895  grpsubsub4  13898  grppnpcan2  13899  grpnpncan  13900  mulgnndir  13954  mulgnn0dir  13955  mulgdir  13957  mulgnnass  13960  mulgnn0ass  13961  mulgass  13962  mulgsubdir  13965  issubg2m  13992  eqgval  14026  qusgrp  14035  cmn32  14107  cmn12  14109  abladdsub  14119  ablsubsub23  14129  prdssgrpd  14191  prdsmndd  14194  rngass  14238  srgdilem  14273  srgass  14275  ringdilem  14316  ringass  14320  opprrng  14382  opprring  14384  mulgass3  14391  unitgrp  14423  dvrass  14446  dvrdir  14450  subrgunit  14547  issubrg2  14549  aprap  14598  lsssn0  14707  islss3  14716  sralmod  14787  restopnb  15282  icnpimaex  15312  cnptopresti  15339  psmettri  15431  isxmet2d  15449  xmettri  15473  metrtri  15478  xmetres2  15480  bldisj  15502  blss2ps  15507  blss2  15508  xmstri2  15571  mstri2  15572  xmstri  15573  mstri  15574  xmstri3  15575  mstri3  15576  msrtri  15577  comet  15600  bdbl  15604  xmetxp  15608  dvconst  15795  dvconstre  15797  dvconstss  15799  sgmmul  16110  gausslemma2dlem1a  16177  pw1ndom3  17020