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  1359  isopolem  5890  caovlem2d  6138  tfrlemibacc  6411  tfrlemibfn  6413  tfr1onlembacc  6427  tfr1onlembfn  6429  tfrcllembacc  6440  tfrcllembfn  6442  eqsupti  7097  prmuloc2  7679  ltntri  8199  elioc2  10057  elico2  10058  elicc2  10059  fseq1p1m1  10215  elfz0ubfz0  10246  ico0  10402  seq3f1olemp  10658  seq3f1oleml  10659  bcval5  10906  isumss2  11646  tanaddap  11992  dvds2ln  12077  divalglemeunn  12174  divalglemex  12175  divalglemeuneg  12176  qredeq  12360  pcdvdstr  12592  isstructr  12789  prdssgrpd  13189  prdsmndd  13222  imasmnd2  13226  mndissubm  13249  grpsubrcan  13355  grpsubadd  13362  grpsubsub  13363  grpaddsubass  13364  grpsubsub4  13367  grpnnncan2  13371  imasgrp2  13388  mulgnndir  13429  mulgnn0dir  13430  mulgdir  13432  mulgnnass  13435  mulgnn0ass  13436  mulgass  13437  mulgsubdir  13440  issubg2m  13467  eqgval  13501  qusgrp  13510  kerf1ghm  13552  cmn32  13582  cmn12  13584  abladdsub  13593  rngass  13643  imasrng  13660  srgass  13675  ringdilem  13716  ringass  13720  imasring  13768  opprrng  13781  opprring  13783  mulgass3  13789  unitgrp  13820  dvrass  13843  dvrdir  13847  subrgunit  13943  issubrg2  13945  aprap  13990  islss3  14083  sralmod  14154  icnpimaex  14625  cnptopresti  14652  upxp  14686  psmettri  14744  isxmet2d  14762  xmettri  14786  metrtri  14791  xmetres2  14793  bldisj  14815  blss2ps  14820  blss2  14821  xmstri2  14884  mstri2  14885  xmstri  14886  mstri  14887  xmstri3  14888  mstri3  14889  msrtri  14890  comet  14913  bdbl  14917  xmetxp  14921  dvconst  15108  dvconstre  15110  dvconstss  15112  sgmmul  15410  findset  15814