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  8455  elioc2  10348  elico2  10349  elicc2  10350  fseq1p1m1  10511  elfz0ubfz0  10542  ico0  10706  seq3f1olemp  10965  seq3f1oleml  10966  bcval5  11215  hashtpgim  11311  swrdsbslen  11452  ccatswrd  11456  isumss2  12176  tanaddap  12522  dvds2ln  12607  divalglemeunn  12704  divalglemex  12705  divalglemeuneg  12706  qredeq  12890  pcdvdstr  13126  isstructr  13416  imasmnd2  13808  mndissubm  13831  grpsubrcan  13935  grpsubadd  13942  grpsubsub  13943  grpaddsubass  13944  grpsubsub4  13947  grpnnncan2  13951  imasgrp2  13962  mulgnndir  14003  mulgnn0dir  14004  mulgdir  14006  mulgnnass  14009  mulgnn0ass  14010  mulgass  14011  mulgsubdir  14014  issubg2m  14041  eqgval  14075  qusgrp  14084  kerf1ghm  14126  cmn32  14156  cmn12  14158  abladdsub  14168  prdssgrpd  14240  prdsmndd  14243  rngass  14287  imasrng  14304  srgass  14324  ringdilem  14365  ringass  14369  imasring  14418  opprrng  14431  opprring  14433  mulgass3  14440  unitgrp  14472  dvrass  14495  dvrdir  14499  subrgunit  14596  issubrg2  14598  aprap  14647  islss3  14765  sralmod  14836  icnpimaex  15361  cnptopresti  15388  upxp  15422  psmettri  15480  isxmet2d  15498  xmettri  15522  metrtri  15527  xmetres2  15529  bldisj  15551  blss2ps  15556  blss2  15557  xmstri2  15620  mstri2  15621  xmstri  15622  mstri  15623  xmstri3  15624  mstri3  15625  msrtri  15626  comet  15649  bdbl  15653  xmetxp  15657  dvconst  15844  dvconstre  15846  dvconstss  15848  sgmmul  16191  findset  17069  pw1ndom3  17118