Theorem simpr1 1034

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simplr1  1070  simprr1  1076  simp1r1  1124  simp2r1  1130  simp3r1  1136  3anandis  1388  isopolem  6028  caovlem2d  6282  suppfnss  6497  tfrlemibacc  6597  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembfn  6628  eqsupti  7337  prmuloc2  7935  ltntri  8456  elioc2  10349  elico2  10350  elicc2  10351  fseq1p1m1  10512  elfz0ubfz0  10543  ico0  10707  seq3f1olemp  10967  seq3f1oleml  10968  bcval5  11217  hashtpgim  11313  swrdsbslen  11454  ccatswrd  11458  isumss2  12179  tanaddap  12525  dvds2ln  12610  divalglemeunn  12707  divalglemex  12708  divalglemeuneg  12709  qredeq  12893  pcdvdstr  13129  isstructr  13419  imasmnd2  13812  mndissubm  13835  grpsubrcan  13939  grpsubadd  13946  grpsubsub  13947  grpaddsubass  13948  grpsubsub4  13951  grpnnncan2  13955  imasgrp2  13966  mulgnndir  14007  mulgnn0dir  14008  mulgdir  14010  mulgnnass  14013  mulgnn0ass  14014  mulgass  14015  mulgsubdir  14018  issubg2m  14045  eqgval  14079  qusgrp  14088  kerf1ghm  14130  cmn32  14191  cmn12  14193  abladdsub  14203  prdssgrpd  14275  prdsmndd  14278  rngass  14322  imasrng  14339  srgass  14359  ringdilem  14400  ringass  14404  imasring  14453  opprrng  14466  opprring  14468  mulgass3  14475  unitgrp  14507  dvrass  14530  dvrdir  14534  subrgunit  14631  issubrg2  14633  aprap  14682  islss3  14800  sralmod  14871  icnpimaex  15403  cnptopresti  15430  upxp  15464  psmettri  15522  isxmet2d  15540  xmettri  15564  metrtri  15569  xmetres2  15571  bldisj  15593  blss2ps  15598  blss2  15599  xmstri2  15662  mstri2  15663  xmstri  15664  mstri  15665  xmstri3  15666  mstri3  15667  msrtri  15668  comet  15691  bdbl  15695  xmetxp  15699  dvconst  15886  dvconstre  15888  dvconstss  15890  sgmmul  16251  findset  17137  pw1ndom3  17186