Theorem simpr1 1006

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981

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 983

This theorem is referenced by:  simplr1  1042  simprr1  1048  simp1r1  1096  simp2r1  1102  simp3r1  1108  3anandis  1360  isopolem  5904  caovlem2d  6152  tfrlemibacc  6425  tfrlemibfn  6427  tfr1onlembacc  6441  tfr1onlembfn  6443  tfrcllembacc  6454  tfrcllembfn  6456  eqsupti  7113  prmuloc2  7700  ltntri  8220  elioc2  10078  elico2  10079  elicc2  10080  fseq1p1m1  10236  elfz0ubfz0  10267  ico0  10426  seq3f1olemp  10682  seq3f1oleml  10683  bcval5  10930  swrdsbslen  11142  ccatswrd  11146  isumss2  11779  tanaddap  12125  dvds2ln  12210  divalglemeunn  12307  divalglemex  12308  divalglemeuneg  12309  qredeq  12493  pcdvdstr  12725  isstructr  12922  prdssgrpd  13322  prdsmndd  13355  imasmnd2  13359  mndissubm  13382  grpsubrcan  13488  grpsubadd  13495  grpsubsub  13496  grpaddsubass  13497  grpsubsub4  13500  grpnnncan2  13504  imasgrp2  13521  mulgnndir  13562  mulgnn0dir  13563  mulgdir  13565  mulgnnass  13568  mulgnn0ass  13569  mulgass  13570  mulgsubdir  13573  issubg2m  13600  eqgval  13634  qusgrp  13643  kerf1ghm  13685  cmn32  13715  cmn12  13717  abladdsub  13726  rngass  13776  imasrng  13793  srgass  13808  ringdilem  13849  ringass  13853  imasring  13901  opprrng  13914  opprring  13916  mulgass3  13922  unitgrp  13953  dvrass  13976  dvrdir  13980  subrgunit  14076  issubrg2  14078  aprap  14123  islss3  14216  sralmod  14287  icnpimaex  14758  cnptopresti  14785  upxp  14819  psmettri  14877  isxmet2d  14895  xmettri  14919  metrtri  14924  xmetres2  14926  bldisj  14948  blss2ps  14953  blss2  14954  xmstri2  15017  mstri2  15018  xmstri  15019  mstri  15020  xmstri3  15021  mstri3  15022  msrtri  15023  comet  15046  bdbl  15050  xmetxp  15054  dvconst  15241  dvconstre  15243  dvconstss  15245  sgmmul  15543  findset  16019