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  6388  tfrlemibfn  6390  tfr1onlembacc  6404  tfr1onlembfn  6406  tfrcllembacc  6417  tfrcllembfn  6419  eqsupti  7066  prmuloc2  7639  ltntri  8159  elioc2  10016  elico2  10017  elicc2  10018  fseq1p1m1  10174  elfz0ubfz0  10205  ico0  10356  seq3f1olemp  10612  seq3f1oleml  10613  bcval5  10860  isumss2  11563  tanaddap  11909  dvds2ln  11994  divalglemeunn  12091  divalglemex  12092  divalglemeuneg  12093  qredeq  12277  pcdvdstr  12509  isstructr  12706  mndissubm  13154  grpsubrcan  13260  grpsubadd  13267  grpsubsub  13268  grpaddsubass  13269  grpsubsub4  13272  grpnnncan2  13276  imasgrp2  13287  mulgnndir  13328  mulgnn0dir  13329  mulgdir  13331  mulgnnass  13334  mulgnn0ass  13335  mulgass  13336  mulgsubdir  13339  issubg2m  13366  eqgval  13400  qusgrp  13409  kerf1ghm  13451  cmn32  13481  cmn12  13483  abladdsub  13492  rngass  13542  imasrng  13559  srgass  13574  ringdilem  13615  ringass  13619  imasring  13667  opprrng  13680  opprring  13682  mulgass3  13688  unitgrp  13719  dvrass  13742  dvrdir  13746  subrgunit  13842  issubrg2  13844  aprap  13889  islss3  13982  sralmod  14053  icnpimaex  14494  cnptopresti  14521  upxp  14555  psmettri  14613  isxmet2d  14631  xmettri  14655  metrtri  14660  xmetres2  14662  bldisj  14684  blss2ps  14689  blss2  14690  xmstri2  14753  mstri2  14754  xmstri  14755  mstri  14756  xmstri3  14757  mstri3  14758  msrtri  14759  comet  14782  bdbl  14786  xmetxp  14790  dvconst  14977  dvconstre  14979  dvconstss  14981  sgmmul  15279  findset  15638