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  5881  tfrlemibacc  6402  tfrlemibfn  6404  tfr1onlembacc  6418  tfr1onlembfn  6420  tfrcllembacc  6431  tfrcllembfn  6433  prltlu  7582  prdisj  7587  prmuloc2  7662  ltntri  8182  eluzuzle  9638  xlesubadd  9987  elioc2  10040  elico2  10041  elicc2  10042  fseq1p1m1  10198  fz0fzelfz0  10231  seq3f1olemp  10641  bcval5  10889  hashdifpr  10946  summodclem2  11612  isumss2  11623  tanaddap  11969  dvds2ln  12054  divalglemeunn  12151  divalglemex  12152  divalglemeuneg  12153  isstructr  12766  f1ovscpbl  13062  prdssgrpd  13165  prdsmndd  13198  mndissubm  13225  grpsubrcan  13331  grpsubadd  13338  grpaddsubass  13340  grpsubsub4  13343  grppnpcan2  13344  grpnpncan  13345  mulgnndir  13405  mulgnn0dir  13406  mulgdir  13408  mulgnnass  13411  mulgnn0ass  13412  mulgass  13413  mulgsubdir  13416  issubg2m  13443  eqgval  13477  qusgrp  13486  cmn32  13558  cmn12  13560  abladdsub  13569  ablsubsub23  13579  rngass  13619  srgdilem  13649  srgass  13651  ringdilem  13692  ringass  13696  opprrng  13757  opprring  13759  mulgass3  13765  unitgrp  13796  dvrass  13819  dvrdir  13823  subrgunit  13919  issubrg2  13921  aprap  13966  lsssn0  14050  islss3  14059  sralmod  14130  restopnb  14571  icnpimaex  14601  cnptopresti  14628  psmettri  14720  isxmet2d  14738  xmettri  14762  metrtri  14767  xmetres2  14769  bldisj  14791  blss2ps  14796  blss2  14797  xmstri2  14860  mstri2  14861  xmstri  14862  mstri  14863  xmstri3  14864  mstri3  14865  msrtri  14866  comet  14889  bdbl  14893  xmetxp  14897  dvconst  15084  dvconstre  15086  dvconstss  15088  sgmmul  15386  gausslemma2dlem1a  15453