Theorem simpr1 1003

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpr1	|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ps )

Proof of Theorem simpr1

Step	Hyp	Ref	Expression
1		simp1 997	. 2 |- ( ( ps /\ ch /\ th ) -> ps )
2	1	adantl 277	1 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ps )

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:  simplr1  1039  simprr1  1045  simp1r1  1093  simp2r1  1099  simp3r1  1105  3anandis  1347  isopolem  5825  caovlem2d  6069  tfrlemibacc  6329  tfrlemibfn  6331  tfr1onlembacc  6345  tfr1onlembfn  6347  tfrcllembacc  6358  tfrcllembfn  6360  eqsupti  6997  prmuloc2  7568  ltntri  8087  elioc2  9938  elico2  9939  elicc2  9940  fseq1p1m1  10096  elfz0ubfz0  10127  ico0  10264  seq3f1olemp  10504  seq3f1oleml  10505  bcval5  10745  isumss2  11403  tanaddap  11749  dvds2ln  11833  divalglemeunn  11928  divalglemex  11929  divalglemeuneg  11930  qredeq  12098  pcdvdstr  12328  isstructr  12479  mndissubm  12871  grpsubrcan  12956  grpsubadd  12963  grpsubsub  12964  grpaddsubass  12965  grpsubsub4  12968  grpnnncan2  12972  mulgnndir  13017  mulgnn0dir  13018  mulgdir  13020  mulgnnass  13023  mulgnn0ass  13024  mulgass  13025  mulgsubdir  13028  issubg2m  13054  eqgval  13087  cmn32  13112  cmn12  13114  abladdsub  13123  srgass  13159  ringdilem  13200  ringass  13204  opprring  13254  mulgass3  13259  unitgrp  13290  dvrass  13313  dvrdir  13317  subrgunit  13365  issubrg2  13367  aprap  13381  islss3  13471  icnpimaex  13796  cnptopresti  13823  upxp  13857  psmettri  13915  isxmet2d  13933  xmettri  13957  metrtri  13962  xmetres2  13964  bldisj  13986  blss2ps  13991  blss2  13992  xmstri2  14055  mstri2  14056  xmstri  14057  mstri  14058  xmstri3  14059  mstri3  14060  msrtri  14061  comet  14084  bdbl  14088  xmetxp  14092  dvconst  14246  findset  14782