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  5813  tfrlemibacc  6317  tfrlemibfn  6319  tfr1onlembacc  6333  tfr1onlembfn  6335  tfrcllembacc  6346  tfrcllembfn  6348  prltlu  7461  prdisj  7466  prmuloc2  7541  ltntri  8059  eluzuzle  9507  xlesubadd  9852  elioc2  9905  elico2  9906  elicc2  9907  fseq1p1m1  10062  fz0fzelfz0  10095  seq3f1olemp  10470  bcval5  10709  hashdifpr  10766  summodclem2  11356  isumss2  11367  tanaddap  11713  dvds2ln  11797  divalglemeunn  11891  divalglemex  11892  divalglemeuneg  11893  isstructr  12442  mndissubm  12726  grpsubrcan  12810  grpsubadd  12817  grpaddsubass  12819  grpsubsub4  12822  grppnpcan2  12823  grpnpncan  12824  mulgnndir  12870  mulgnn0dir  12871  mulgdir  12873  mulgnnass  12876  mulgnn0ass  12877  mulgass  12878  mulgsubdir  12881  cmn32  12903  cmn12  12905  abladdsub  12914  ablsubsub23  12924  srgdilem  12945  srgass  12947  ringdilem  12988  ringass  12992  restopnb  13232  icnpimaex  13262  cnptopresti  13289  psmettri  13381  isxmet2d  13399  xmettri  13423  metrtri  13428  xmetres2  13430  bldisj  13452  blss2ps  13457  blss2  13458  xmstri2  13521  mstri2  13522  xmstri  13523  mstri  13524  xmstri3  13525  mstri3  13526  msrtri  13527  comet  13550  bdbl  13554  xmetxp  13558  dvconst  13712