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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simplr1  1070  simprr1  1076  simp1r1  1124  simp2r1  1130  simp3r1  1136  3anandis  1388  isopolem  6028  caovlem2d  6282  suppfnss  6497  tfrlemibacc  6597  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembfn  6628  eqsupti  7336  prmuloc2  7934  ltntri  8454  elioc2  10338  elico2  10339  elicc2  10340  fseq1p1m1  10501  elfz0ubfz0  10532  ico0  10696  seq3f1olemp  10952  seq3f1oleml  10953  bcval5  11201  hashtpgim  11297  swrdsbslen  11438  ccatswrd  11442  isumss2  12160  tanaddap  12506  dvds2ln  12591  divalglemeunn  12688  divalglemex  12689  divalglemeuneg  12690  qredeq  12874  pcdvdstr  13106  isstructr  13367  imasmnd2  13759  mndissubm  13782  grpsubrcan  13886  grpsubadd  13893  grpsubsub  13894  grpaddsubass  13895  grpsubsub4  13898  grpnnncan2  13902  imasgrp2  13913  mulgnndir  13954  mulgnn0dir  13955  mulgdir  13957  mulgnnass  13960  mulgnn0ass  13961  mulgass  13962  mulgsubdir  13965  issubg2m  13992  eqgval  14026  qusgrp  14035  kerf1ghm  14077  cmn32  14107  cmn12  14109  abladdsub  14119  prdssgrpd  14191  prdsmndd  14194  rngass  14238  imasrng  14255  srgass  14275  ringdilem  14316  ringass  14320  imasring  14369  opprrng  14382  opprring  14384  mulgass3  14391  unitgrp  14423  dvrass  14446  dvrdir  14450  subrgunit  14547  issubrg2  14549  aprap  14598  islss3  14716  sralmod  14787  icnpimaex  15312  cnptopresti  15339  upxp  15373  psmettri  15431  isxmet2d  15449  xmettri  15473  metrtri  15478  xmetres2  15480  bldisj  15502  blss2ps  15507  blss2  15508  xmstri2  15571  mstri2  15572  xmstri  15573  mstri  15574  xmstri3  15575  mstri3  15576  msrtri  15577  comet  15600  bdbl  15604  xmetxp  15608  dvconst  15795  dvconstre  15797  dvconstss  15799  sgmmul  16110  findset  16971  pw1ndom3  17020