Theorem simpr1 1034

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

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

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 1011

This theorem is referenced by:  simplr1  1070  simprr1  1076  simp1r1  1124  simp2r1  1130  simp3r1  1136  3anandis  1388  isopolem  6018  caovlem2d  6272  suppfnss  6487  tfrlemibacc  6587  tfrlemibfn  6589  tfr1onlembacc  6603  tfr1onlembfn  6605  tfrcllembacc  6616  tfrcllembfn  6618  eqsupti  7326  prmuloc2  7924  ltntri  8444  elioc2  10317  elico2  10318  elicc2  10319  fseq1p1m1  10479  elfz0ubfz0  10510  ico0  10674  seq3f1olemp  10930  seq3f1oleml  10931  bcval5  11179  hashtpgim  11275  swrdsbslen  11416  ccatswrd  11420  isumss2  12138  tanaddap  12484  dvds2ln  12569  divalglemeunn  12666  divalglemex  12667  divalglemeuneg  12668  qredeq  12852  pcdvdstr  13084  isstructr  13345  imasmnd2  13736  mndissubm  13759  grpsubrcan  13863  grpsubadd  13870  grpsubsub  13871  grpaddsubass  13872  grpsubsub4  13875  grpnnncan2  13879  imasgrp2  13890  mulgnndir  13931  mulgnn0dir  13932  mulgdir  13934  mulgnnass  13937  mulgnn0ass  13938  mulgass  13939  mulgsubdir  13942  issubg2m  13969  eqgval  14003  qusgrp  14012  kerf1ghm  14054  cmn32  14084  cmn12  14086  abladdsub  14096  prdssgrpd  14168  prdsmndd  14171  rngass  14213  imasrng  14230  srgass  14249  ringdilem  14290  ringass  14294  imasring  14342  opprrng  14355  opprring  14357  mulgass3  14364  unitgrp  14396  dvrass  14419  dvrdir  14423  subrgunit  14520  issubrg2  14522  aprap  14571  islss3  14688  sralmod  14759  icnpimaex  15235  cnptopresti  15262  upxp  15296  psmettri  15354  isxmet2d  15372  xmettri  15396  metrtri  15401  xmetres2  15403  bldisj  15425  blss2ps  15430  blss2  15431  xmstri2  15494  mstri2  15495  xmstri  15496  mstri  15497  xmstri3  15498  mstri3  15499  msrtri  15500  comet  15523  bdbl  15527  xmetxp  15531  dvconst  15718  dvconstre  15720  dvconstss  15722  sgmmul  16024  findset  16885  pw1ndom3  16934