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  1358  isopolem  5865  caovlem2d  6111  tfrlemibacc  6379  tfrlemibfn  6381  tfr1onlembacc  6395  tfr1onlembfn  6397  tfrcllembacc  6408  tfrcllembfn  6410  eqsupti  7055  prmuloc2  7627  ltntri  8147  elioc2  10002  elico2  10003  elicc2  10004  fseq1p1m1  10160  elfz0ubfz0  10191  ico0  10330  seq3f1olemp  10586  seq3f1oleml  10587  bcval5  10834  isumss2  11536  tanaddap  11882  dvds2ln  11967  divalglemeunn  12062  divalglemex  12063  divalglemeuneg  12064  qredeq  12234  pcdvdstr  12465  isstructr  12633  mndissubm  13047  grpsubrcan  13153  grpsubadd  13160  grpsubsub  13161  grpaddsubass  13162  grpsubsub4  13165  grpnnncan2  13169  imasgrp2  13180  mulgnndir  13221  mulgnn0dir  13222  mulgdir  13224  mulgnnass  13227  mulgnn0ass  13228  mulgass  13229  mulgsubdir  13232  issubg2m  13259  eqgval  13293  qusgrp  13302  kerf1ghm  13344  cmn32  13374  cmn12  13376  abladdsub  13385  rngass  13435  imasrng  13452  srgass  13467  ringdilem  13508  ringass  13512  imasring  13560  opprrng  13573  opprring  13575  mulgass3  13581  unitgrp  13612  dvrass  13635  dvrdir  13639  subrgunit  13735  issubrg2  13737  aprap  13782  islss3  13875  sralmod  13946  icnpimaex  14379  cnptopresti  14406  upxp  14440  psmettri  14498  isxmet2d  14516  xmettri  14540  metrtri  14545  xmetres2  14547  bldisj  14569  blss2ps  14574  blss2  14575  xmstri2  14638  mstri2  14639  xmstri  14640  mstri  14641  xmstri3  14642  mstri3  14643  msrtri  14644  comet  14667  bdbl  14671  xmetxp  14675  dvconst  14846  findset  15437