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  5866  caovlem2d  6113  tfrlemibacc  6381  tfrlemibfn  6383  tfr1onlembacc  6397  tfr1onlembfn  6399  tfrcllembacc  6410  tfrcllembfn  6412  eqsupti  7057  prmuloc2  7629  ltntri  8149  elioc2  10005  elico2  10006  elicc2  10007  fseq1p1m1  10163  elfz0ubfz0  10194  ico0  10333  seq3f1olemp  10589  seq3f1oleml  10590  bcval5  10837  isumss2  11539  tanaddap  11885  dvds2ln  11970  divalglemeunn  12065  divalglemex  12066  divalglemeuneg  12067  qredeq  12237  pcdvdstr  12468  isstructr  12636  mndissubm  13050  grpsubrcan  13156  grpsubadd  13163  grpsubsub  13164  grpaddsubass  13165  grpsubsub4  13168  grpnnncan2  13172  imasgrp2  13183  mulgnndir  13224  mulgnn0dir  13225  mulgdir  13227  mulgnnass  13230  mulgnn0ass  13231  mulgass  13232  mulgsubdir  13235  issubg2m  13262  eqgval  13296  qusgrp  13305  kerf1ghm  13347  cmn32  13377  cmn12  13379  abladdsub  13388  rngass  13438  imasrng  13455  srgass  13470  ringdilem  13511  ringass  13515  imasring  13563  opprrng  13576  opprring  13578  mulgass3  13584  unitgrp  13615  dvrass  13638  dvrdir  13642  subrgunit  13738  issubrg2  13740  aprap  13785  islss3  13878  sralmod  13949  icnpimaex  14390  cnptopresti  14417  upxp  14451  psmettri  14509  isxmet2d  14527  xmettri  14551  metrtri  14556  xmetres2  14558  bldisj  14580  blss2ps  14585  blss2  14586  xmstri2  14649  mstri2  14650  xmstri  14651  mstri  14652  xmstri3  14653  mstri3  14654  msrtri  14655  comet  14678  bdbl  14682  xmetxp  14686  dvconst  14873  dvconstre  14875  dvconstss  14877  findset  15507