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  1359  isopolem  5890  caovlem2d  6138  tfrlemibacc  6411  tfrlemibfn  6413  tfr1onlembacc  6427  tfr1onlembfn  6429  tfrcllembacc  6440  tfrcllembfn  6442  eqsupti  7097  prmuloc2  7679  ltntri  8199  elioc2  10057  elico2  10058  elicc2  10059  fseq1p1m1  10215  elfz0ubfz0  10246  ico0  10402  seq3f1olemp  10658  seq3f1oleml  10659  bcval5  10906  isumss2  11675  tanaddap  12021  dvds2ln  12106  divalglemeunn  12203  divalglemex  12204  divalglemeuneg  12205  qredeq  12389  pcdvdstr  12621  isstructr  12818  prdssgrpd  13218  prdsmndd  13251  imasmnd2  13255  mndissubm  13278  grpsubrcan  13384  grpsubadd  13391  grpsubsub  13392  grpaddsubass  13393  grpsubsub4  13396  grpnnncan2  13400  imasgrp2  13417  mulgnndir  13458  mulgnn0dir  13459  mulgdir  13461  mulgnnass  13464  mulgnn0ass  13465  mulgass  13466  mulgsubdir  13469  issubg2m  13496  eqgval  13530  qusgrp  13539  kerf1ghm  13581  cmn32  13611  cmn12  13613  abladdsub  13622  rngass  13672  imasrng  13689  srgass  13704  ringdilem  13745  ringass  13749  imasring  13797  opprrng  13810  opprring  13812  mulgass3  13818  unitgrp  13849  dvrass  13872  dvrdir  13876  subrgunit  13972  issubrg2  13974  aprap  14019  islss3  14112  sralmod  14183  icnpimaex  14654  cnptopresti  14681  upxp  14715  psmettri  14773  isxmet2d  14791  xmettri  14815  metrtri  14820  xmetres2  14822  bldisj  14844  blss2ps  14849  blss2  14850  xmstri2  14913  mstri2  14914  xmstri  14915  mstri  14916  xmstri3  14917  mstri3  14918  msrtri  14919  comet  14942  bdbl  14946  xmetxp  14950  dvconst  15137  dvconstre  15139  dvconstss  15141  sgmmul  15439  findset  15843