Theorem simpr1 1005

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

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:  simplr1  1041  simprr1  1047  simp1r1  1095  simp2r1  1101  simp3r1  1107  3anandis  1358  isopolem  5872  caovlem2d  6120  tfrlemibacc  6393  tfrlemibfn  6395  tfr1onlembacc  6409  tfr1onlembfn  6411  tfrcllembacc  6422  tfrcllembfn  6424  eqsupti  7071  prmuloc2  7653  ltntri  8173  elioc2  10030  elico2  10031  elicc2  10032  fseq1p1m1  10188  elfz0ubfz0  10219  ico0  10370  seq3f1olemp  10626  seq3f1oleml  10627  bcval5  10874  isumss2  11577  tanaddap  11923  dvds2ln  12008  divalglemeunn  12105  divalglemex  12106  divalglemeuneg  12107  qredeq  12291  pcdvdstr  12523  isstructr  12720  prdssgrpd  13119  prdsmndd  13152  imasmnd2  13156  mndissubm  13179  grpsubrcan  13285  grpsubadd  13292  grpsubsub  13293  grpaddsubass  13294  grpsubsub4  13297  grpnnncan2  13301  imasgrp2  13318  mulgnndir  13359  mulgnn0dir  13360  mulgdir  13362  mulgnnass  13365  mulgnn0ass  13366  mulgass  13367  mulgsubdir  13370  issubg2m  13397  eqgval  13431  qusgrp  13440  kerf1ghm  13482  cmn32  13512  cmn12  13514  abladdsub  13523  rngass  13573  imasrng  13590  srgass  13605  ringdilem  13646  ringass  13650  imasring  13698  opprrng  13711  opprring  13713  mulgass3  13719  unitgrp  13750  dvrass  13773  dvrdir  13777  subrgunit  13873  issubrg2  13875  aprap  13920  islss3  14013  sralmod  14084  icnpimaex  14555  cnptopresti  14582  upxp  14616  psmettri  14674  isxmet2d  14692  xmettri  14716  metrtri  14721  xmetres2  14723  bldisj  14745  blss2ps  14750  blss2  14751  xmstri2  14814  mstri2  14815  xmstri  14816  mstri  14817  xmstri3  14818  mstri3  14819  msrtri  14820  comet  14843  bdbl  14847  xmetxp  14851  dvconst  15038  dvconstre  15040  dvconstss  15042  sgmmul  15340  findset  15699