Theorem simpr1 1004

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

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

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 981

This theorem is referenced by:  simplr1  1040  simprr1  1046  simp1r1  1094  simp2r1  1100  simp3r1  1106  3anandis  1357  isopolem  5836  caovlem2d  6081  tfrlemibacc  6341  tfrlemibfn  6343  tfr1onlembacc  6357  tfr1onlembfn  6359  tfrcllembacc  6370  tfrcllembfn  6372  eqsupti  7009  prmuloc2  7580  ltntri  8099  elioc2  9950  elico2  9951  elicc2  9952  fseq1p1m1  10108  elfz0ubfz0  10139  ico0  10276  seq3f1olemp  10516  seq3f1oleml  10517  bcval5  10757  isumss2  11415  tanaddap  11761  dvds2ln  11845  divalglemeunn  11940  divalglemex  11941  divalglemeuneg  11942  qredeq  12110  pcdvdstr  12340  isstructr  12491  mndissubm  12888  grpsubrcan  12978  grpsubadd  12985  grpsubsub  12986  grpaddsubass  12987  grpsubsub4  12990  grpnnncan2  12994  imasgrp2  13005  mulgnndir  13044  mulgnn0dir  13045  mulgdir  13047  mulgnnass  13050  mulgnn0ass  13051  mulgass  13052  mulgsubdir  13055  issubg2m  13081  eqgval  13115  cmn32  13141  cmn12  13143  abladdsub  13152  rngass  13191  imasrng  13208  srgass  13223  ringdilem  13264  ringass  13268  imasring  13312  opprrng  13325  opprring  13327  mulgass3  13333  unitgrp  13364  dvrass  13387  dvrdir  13391  subrgunit  13459  issubrg2  13461  aprap  13475  islss3  13568  sralmod  13639  icnpimaex  14007  cnptopresti  14034  upxp  14068  psmettri  14126  isxmet2d  14144  xmettri  14168  metrtri  14173  xmetres2  14175  bldisj  14197  blss2ps  14202  blss2  14203  xmstri2  14266  mstri2  14267  xmstri  14268  mstri  14269  xmstri3  14270  mstri3  14271  msrtri  14272  comet  14295  bdbl  14299  xmetxp  14303  dvconst  14457  findset  14993