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  7651  ltntri  8171  elioc2  10028  elico2  10029  elicc2  10030  fseq1p1m1  10186  elfz0ubfz0  10217  ico0  10368  seq3f1olemp  10624  seq3f1oleml  10625  bcval5  10872  isumss2  11575  tanaddap  11921  dvds2ln  12006  divalglemeunn  12103  divalglemex  12104  divalglemeuneg  12105  qredeq  12289  pcdvdstr  12521  isstructr  12718  prdssgrpd  13117  prdsmndd  13150  imasmnd2  13154  mndissubm  13177  grpsubrcan  13283  grpsubadd  13290  grpsubsub  13291  grpaddsubass  13292  grpsubsub4  13295  grpnnncan2  13299  imasgrp2  13316  mulgnndir  13357  mulgnn0dir  13358  mulgdir  13360  mulgnnass  13363  mulgnn0ass  13364  mulgass  13365  mulgsubdir  13368  issubg2m  13395  eqgval  13429  qusgrp  13438  kerf1ghm  13480  cmn32  13510  cmn12  13512  abladdsub  13521  rngass  13571  imasrng  13588  srgass  13603  ringdilem  13644  ringass  13648  imasring  13696  opprrng  13709  opprring  13711  mulgass3  13717  unitgrp  13748  dvrass  13771  dvrdir  13775  subrgunit  13871  issubrg2  13873  aprap  13918  islss3  14011  sralmod  14082  icnpimaex  14531  cnptopresti  14558  upxp  14592  psmettri  14650  isxmet2d  14668  xmettri  14692  metrtri  14697  xmetres2  14699  bldisj  14721  blss2ps  14726  blss2  14727  xmstri2  14790  mstri2  14791  xmstri  14792  mstri  14793  xmstri3  14794  mstri3  14795  msrtri  14796  comet  14819  bdbl  14823  xmetxp  14827  dvconst  15014  dvconstre  15016  dvconstss  15018  sgmmul  15316  findset  15675