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  7855  prdisj  7860  prmuloc2  7935  ltntri  8456  eluzuzle  9940  xlesubadd  10296  elioc2  10349  elico2  10350  elicc2  10351  fseq1p1m1  10512  fz0fzelfz0  10545  seq3f1olemp  10967  bcval5  11217  hashdifpr  11277  hashtpgim  11313  swrdsbslen  11454  ccatswrd  11458  swrdswrdlem  11492  summodclem2  12168  isumss2  12179  tanaddap  12525  dvds2ln  12610  divalglemeunn  12707  divalglemex  12708  divalglemeuneg  12709  isstructr  13419  f1ovscpbl  13686  mndissubm  13835  grpsubrcan  13939  grpsubadd  13946  grpaddsubass  13948  grpsubsub4  13951  grppnpcan2  13952  grpnpncan  13953  mulgnndir  14007  mulgnn0dir  14008  mulgdir  14010  mulgnnass  14013  mulgnn0ass  14014  mulgass  14015  mulgsubdir  14018  issubg2m  14045  eqgval  14079  qusgrp  14088  cmn32  14191  cmn12  14193  abladdsub  14203  ablsubsub23  14213  prdssgrpd  14275  prdsmndd  14278  rngass  14322  srgdilem  14357  srgass  14359  ringdilem  14400  ringass  14404  opprrng  14466  opprring  14468  mulgass3  14475  unitgrp  14507  dvrass  14530  dvrdir  14534  subrgunit  14631  issubrg2  14633  aprap  14682  lsssn0  14791  islss3  14800  sralmod  14871  restopnb  15373  icnpimaex  15403  cnptopresti  15430  psmettri  15522  isxmet2d  15540  xmettri  15564  metrtri  15569  xmetres2  15571  bldisj  15593  blss2ps  15598  blss2  15599  xmstri2  15662  mstri2  15663  xmstri  15664  mstri  15665  xmstri3  15666  mstri3  15667  msrtri  15668  comet  15691  bdbl  15695  xmetxp  15699  dvconst  15886  dvconstre  15888  dvconstss  15890  sgmmul  16251  gausslemma2dlem1a  16343  pw1ndom3  17186