Theorem simpr1 1029

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

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

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 1006

This theorem is referenced by:  simplr1  1065  simprr1  1071  simp1r1  1119  simp2r1  1125  simp3r1  1131  3anandis  1383  isopolem  5963  caovlem2d  6215  tfrlemibacc  6492  tfrlemibfn  6494  tfr1onlembacc  6508  tfr1onlembfn  6510  tfrcllembacc  6521  tfrcllembfn  6523  eqsupti  7195  prmuloc2  7787  ltntri  8307  elioc2  10171  elico2  10172  elicc2  10173  fseq1p1m1  10329  elfz0ubfz0  10360  ico0  10522  seq3f1olemp  10778  seq3f1oleml  10779  bcval5  11026  hashtpgim  11110  swrdsbslen  11251  ccatswrd  11255  isumss2  11972  tanaddap  12318  dvds2ln  12403  divalglemeunn  12500  divalglemex  12501  divalglemeuneg  12502  qredeq  12686  pcdvdstr  12918  isstructr  13115  prdssgrpd  13516  prdsmndd  13549  imasmnd2  13553  mndissubm  13576  grpsubrcan  13682  grpsubadd  13689  grpsubsub  13690  grpaddsubass  13691  grpsubsub4  13694  grpnnncan2  13698  imasgrp2  13715  mulgnndir  13756  mulgnn0dir  13757  mulgdir  13759  mulgnnass  13762  mulgnn0ass  13763  mulgass  13764  mulgsubdir  13767  issubg2m  13794  eqgval  13828  qusgrp  13837  kerf1ghm  13879  cmn32  13909  cmn12  13911  abladdsub  13920  rngass  13971  imasrng  13988  srgass  14003  ringdilem  14044  ringass  14048  imasring  14096  opprrng  14109  opprring  14111  mulgass3  14117  unitgrp  14149  dvrass  14172  dvrdir  14176  subrgunit  14272  issubrg2  14274  aprap  14319  islss3  14412  sralmod  14483  icnpimaex  14954  cnptopresti  14981  upxp  15015  psmettri  15073  isxmet2d  15091  xmettri  15115  metrtri  15120  xmetres2  15122  bldisj  15144  blss2ps  15149  blss2  15150  xmstri2  15213  mstri2  15214  xmstri  15215  mstri  15216  xmstri3  15217  mstri3  15218  msrtri  15219  comet  15242  bdbl  15246  xmetxp  15250  dvconst  15437  dvconstre  15439  dvconstss  15441  sgmmul  15739  findset  16591  pw1ndom3  16640