Theorem simpr1 1030

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

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

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 1007

This theorem is referenced by:  simplr1  1066  simprr1  1072  simp1r1  1120  simp2r1  1126  simp3r1  1132  3anandis  1384  isopolem  5973  caovlem2d  6225  suppfnss  6435  tfrlemibacc  6535  tfrlemibfn  6537  tfr1onlembacc  6551  tfr1onlembfn  6553  tfrcllembacc  6564  tfrcllembfn  6566  eqsupti  7238  prmuloc2  7830  ltntri  8349  elioc2  10215  elico2  10216  elicc2  10217  fseq1p1m1  10374  elfz0ubfz0  10405  ico0  10567  seq3f1olemp  10823  seq3f1oleml  10824  bcval5  11071  hashtpgim  11155  swrdsbslen  11296  ccatswrd  11300  isumss2  12017  tanaddap  12363  dvds2ln  12448  divalglemeunn  12545  divalglemex  12546  divalglemeuneg  12547  qredeq  12731  pcdvdstr  12963  isstructr  13160  prdssgrpd  13561  prdsmndd  13594  imasmnd2  13598  mndissubm  13621  grpsubrcan  13727  grpsubadd  13734  grpsubsub  13735  grpaddsubass  13736  grpsubsub4  13739  grpnnncan2  13743  imasgrp2  13760  mulgnndir  13801  mulgnn0dir  13802  mulgdir  13804  mulgnnass  13807  mulgnn0ass  13808  mulgass  13809  mulgsubdir  13812  issubg2m  13839  eqgval  13873  qusgrp  13882  kerf1ghm  13924  cmn32  13954  cmn12  13956  abladdsub  13965  rngass  14016  imasrng  14033  srgass  14048  ringdilem  14089  ringass  14093  imasring  14141  opprrng  14154  opprring  14156  mulgass3  14162  unitgrp  14194  dvrass  14217  dvrdir  14221  subrgunit  14317  issubrg2  14319  aprap  14365  islss3  14458  sralmod  14529  icnpimaex  15005  cnptopresti  15032  upxp  15066  psmettri  15124  isxmet2d  15142  xmettri  15166  metrtri  15171  xmetres2  15173  bldisj  15195  blss2ps  15200  blss2  15201  xmstri2  15264  mstri2  15265  xmstri  15266  mstri  15267  xmstri3  15268  mstri3  15269  msrtri  15270  comet  15293  bdbl  15297  xmetxp  15301  dvconst  15488  dvconstre  15490  dvconstss  15492  sgmmul  15793  findset  16644  pw1ndom3  16693