Theorem simpr2 1006

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

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

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 982

This theorem is referenced by:  simplr2  1042  simprr2  1048  simp1r2  1096  simp2r2  1102  simp3r2  1108  3anandis  1359  isopolem  5890  tfrlemibacc  6411  tfrlemibfn  6413  tfr1onlembacc  6427  tfr1onlembfn  6429  tfrcllembacc  6440  tfrcllembfn  6442  prltlu  7599  prdisj  7604  prmuloc2  7679  ltntri  8199  eluzuzle  9655  xlesubadd  10004  elioc2  10057  elico2  10058  elicc2  10059  fseq1p1m1  10215  fz0fzelfz0  10248  seq3f1olemp  10658  bcval5  10906  hashdifpr  10963  summodclem2  11635  isumss2  11646  tanaddap  11992  dvds2ln  12077  divalglemeunn  12174  divalglemex  12175  divalglemeuneg  12176  isstructr  12789  f1ovscpbl  13086  prdssgrpd  13189  prdsmndd  13222  mndissubm  13249  grpsubrcan  13355  grpsubadd  13362  grpaddsubass  13364  grpsubsub4  13367  grppnpcan2  13368  grpnpncan  13369  mulgnndir  13429  mulgnn0dir  13430  mulgdir  13432  mulgnnass  13435  mulgnn0ass  13436  mulgass  13437  mulgsubdir  13440  issubg2m  13467  eqgval  13501  qusgrp  13510  cmn32  13582  cmn12  13584  abladdsub  13593  ablsubsub23  13603  rngass  13643  srgdilem  13673  srgass  13675  ringdilem  13716  ringass  13720  opprrng  13781  opprring  13783  mulgass3  13789  unitgrp  13820  dvrass  13843  dvrdir  13847  subrgunit  13943  issubrg2  13945  aprap  13990  lsssn0  14074  islss3  14083  sralmod  14154  restopnb  14595  icnpimaex  14625  cnptopresti  14652  psmettri  14744  isxmet2d  14762  xmettri  14786  metrtri  14791  xmetres2  14793  bldisj  14815  blss2ps  14820  blss2  14821  xmstri2  14884  mstri2  14885  xmstri  14886  mstri  14887  xmstri3  14888  mstri3  14889  msrtri  14890  comet  14913  bdbl  14917  xmetxp  14921  dvconst  15108  dvconstre  15110  dvconstss  15112  sgmmul  15410  gausslemma2dlem1a  15477