Theorem simpr2 1004

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

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

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 980

This theorem is referenced by:  simplr2  1040  simprr2  1046  simp1r2  1094  simp2r2  1100  simp3r2  1106  3anandis  1347  isopolem  5822  tfrlemibacc  6326  tfrlemibfn  6328  tfr1onlembacc  6342  tfr1onlembfn  6344  tfrcllembacc  6355  tfrcllembfn  6357  prltlu  7485  prdisj  7490  prmuloc2  7565  ltntri  8084  eluzuzle  9535  xlesubadd  9882  elioc2  9935  elico2  9936  elicc2  9937  fseq1p1m1  10093  fz0fzelfz0  10126  seq3f1olemp  10501  bcval5  10742  hashdifpr  10799  summodclem2  11389  isumss2  11400  tanaddap  11746  dvds2ln  11830  divalglemeunn  11925  divalglemex  11926  divalglemeuneg  11927  isstructr  12476  f1ovscpbl  12732  mndissubm  12865  grpsubrcan  12950  grpsubadd  12957  grpaddsubass  12959  grpsubsub4  12962  grppnpcan2  12963  grpnpncan  12964  mulgnndir  13010  mulgnn0dir  13011  mulgdir  13013  mulgnnass  13016  mulgnn0ass  13017  mulgass  13018  mulgsubdir  13021  issubg2m  13047  eqgval  13080  cmn32  13105  cmn12  13107  abladdsub  13116  ablsubsub23  13126  srgdilem  13150  srgass  13152  ringdilem  13193  ringass  13197  opprring  13247  mulgass3  13252  unitgrp  13283  dvrass  13306  dvrdir  13310  subrgunit  13358  issubrg2  13360  aprap  13374  restopnb  13651  icnpimaex  13681  cnptopresti  13708  psmettri  13800  isxmet2d  13818  xmettri  13842  metrtri  13847  xmetres2  13849  bldisj  13871  blss2ps  13876  blss2  13877  xmstri2  13940  mstri2  13941  xmstri  13942  mstri  13943  xmstri3  13944  mstri3  13945  msrtri  13946  comet  13969  bdbl  13973  xmetxp  13977  dvconst  14131