Theorem simpr1 1029

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

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

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 1006

This theorem is referenced by:  simplr1  1065  simprr1  1071  simp1r1  1119  simp2r1  1125  simp3r1  1131  3anandis  1383  isopolem  5963  caovlem2d  6215  tfrlemibacc  6492  tfrlemibfn  6494  tfr1onlembacc  6508  tfr1onlembfn  6510  tfrcllembacc  6521  tfrcllembfn  6523  eqsupti  7195  prmuloc2  7787  ltntri  8307  elioc2  10171  elico2  10172  elicc2  10173  fseq1p1m1  10329  elfz0ubfz0  10360  ico0  10521  seq3f1olemp  10777  seq3f1oleml  10778  bcval5  11025  swrdsbslen  11247  ccatswrd  11251  isumss2  11955  tanaddap  12301  dvds2ln  12386  divalglemeunn  12483  divalglemex  12484  divalglemeuneg  12485  qredeq  12669  pcdvdstr  12901  isstructr  13098  prdssgrpd  13499  prdsmndd  13532  imasmnd2  13536  mndissubm  13559  grpsubrcan  13665  grpsubadd  13672  grpsubsub  13673  grpaddsubass  13674  grpsubsub4  13677  grpnnncan2  13681  imasgrp2  13698  mulgnndir  13739  mulgnn0dir  13740  mulgdir  13742  mulgnnass  13745  mulgnn0ass  13746  mulgass  13747  mulgsubdir  13750  issubg2m  13777  eqgval  13811  qusgrp  13820  kerf1ghm  13862  cmn32  13892  cmn12  13894  abladdsub  13903  rngass  13954  imasrng  13971  srgass  13986  ringdilem  14027  ringass  14031  imasring  14079  opprrng  14092  opprring  14094  mulgass3  14100  unitgrp  14132  dvrass  14155  dvrdir  14159  subrgunit  14255  issubrg2  14257  aprap  14302  islss3  14395  sralmod  14466  icnpimaex  14937  cnptopresti  14964  upxp  14998  psmettri  15056  isxmet2d  15074  xmettri  15098  metrtri  15103  xmetres2  15105  bldisj  15127  blss2ps  15132  blss2  15133  xmstri2  15196  mstri2  15197  xmstri  15198  mstri  15199  xmstri3  15200  mstri3  15201  msrtri  15202  comet  15225  bdbl  15229  xmetxp  15233  dvconst  15420  dvconstre  15422  dvconstss  15424  sgmmul  15722  findset  16543  pw1ndom3  16592