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  5995  caovlem2d  6247  suppfnss  6457  tfrlemibacc  6557  tfrlemibfn  6559  tfr1onlembacc  6573  tfr1onlembfn  6575  tfrcllembacc  6586  tfrcllembfn  6588  eqsupti  7287  prmuloc2  7882  ltntri  8401  elioc2  10269  elico2  10270  elicc2  10271  fseq1p1m1  10428  elfz0ubfz0  10459  ico0  10621  seq3f1olemp  10877  seq3f1oleml  10878  bcval5  11125  hashtpgim  11217  swrdsbslen  11358  ccatswrd  11362  isumss2  12079  tanaddap  12425  dvds2ln  12510  divalglemeunn  12607  divalglemex  12608  divalglemeuneg  12609  qredeq  12793  pcdvdstr  13025  isstructr  13227  prdssgrpd  13628  prdsmndd  13661  imasmnd2  13665  mndissubm  13688  grpsubrcan  13794  grpsubadd  13801  grpsubsub  13802  grpaddsubass  13803  grpsubsub4  13806  grpnnncan2  13810  imasgrp2  13827  mulgnndir  13868  mulgnn0dir  13869  mulgdir  13871  mulgnnass  13874  mulgnn0ass  13875  mulgass  13876  mulgsubdir  13879  issubg2m  13906  eqgval  13940  qusgrp  13949  kerf1ghm  13991  cmn32  14021  cmn12  14023  abladdsub  14032  rngass  14083  imasrng  14100  srgass  14115  ringdilem  14156  ringass  14160  imasring  14208  opprrng  14221  opprring  14223  mulgass3  14229  unitgrp  14261  dvrass  14284  dvrdir  14288  subrgunit  14384  issubrg2  14386  aprap  14432  islss3  14527  sralmod  14598  icnpimaex  15076  cnptopresti  15103  upxp  15137  psmettri  15195  isxmet2d  15213  xmettri  15237  metrtri  15242  xmetres2  15244  bldisj  15266  blss2ps  15271  blss2  15272  xmstri2  15335  mstri2  15336  xmstri  15337  mstri  15338  xmstri3  15339  mstri3  15340  msrtri  15341  comet  15364  bdbl  15368  xmetxp  15372  dvconst  15559  dvconstre  15561  dvconstss  15563  sgmmul  15864  findset  16715  pw1ndom3  16764