Theorem simpr1 1030

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

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

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 1007

This theorem is referenced by:  simplr1  1066  simprr1  1072  simp1r1  1120  simp2r1  1126  simp3r1  1132  3anandis  1384  isopolem  6001  caovlem2d  6255  suppfnss  6470  tfrlemibacc  6570  tfrlemibfn  6572  tfr1onlembacc  6586  tfr1onlembfn  6588  tfrcllembacc  6599  tfrcllembfn  6601  eqsupti  7300  prmuloc2  7898  ltntri  8417  elioc2  10288  elico2  10289  elicc2  10290  fseq1p1m1  10450  elfz0ubfz0  10481  ico0  10645  seq3f1olemp  10901  seq3f1oleml  10902  bcval5  11150  hashtpgim  11242  swrdsbslen  11383  ccatswrd  11387  isumss2  12104  tanaddap  12450  dvds2ln  12535  divalglemeunn  12632  divalglemex  12633  divalglemeuneg  12634  qredeq  12818  pcdvdstr  13050  isstructr  13311  imasmnd2  13707  mndissubm  13730  grpsubrcan  13836  grpsubadd  13843  grpsubsub  13844  grpaddsubass  13845  grpsubsub4  13848  grpnnncan2  13852  imasgrp2  13863  mulgnndir  13904  mulgnn0dir  13905  mulgdir  13907  mulgnnass  13910  mulgnn0ass  13911  mulgass  13912  mulgsubdir  13915  issubg2m  13942  eqgval  13976  qusgrp  13985  kerf1ghm  14027  cmn32  14057  cmn12  14059  abladdsub  14068  prdssgrpd  14133  prdsmndd  14136  rngass  14178  imasrng  14195  srgass  14214  ringdilem  14255  ringass  14259  imasring  14307  opprrng  14320  opprring  14322  mulgass3  14329  unitgrp  14361  dvrass  14384  dvrdir  14388  subrgunit  14485  issubrg2  14487  aprap  14536  islss3  14653  sralmod  14724  icnpimaex  15202  cnptopresti  15229  upxp  15263  psmettri  15321  isxmet2d  15339  xmettri  15363  metrtri  15368  xmetres2  15370  bldisj  15392  blss2ps  15397  blss2  15398  xmstri2  15461  mstri2  15462  xmstri  15463  mstri  15464  xmstri3  15465  mstri3  15466  msrtri  15467  comet  15490  bdbl  15494  xmetxp  15498  dvconst  15685  dvconstre  15687  dvconstss  15689  sgmmul  15990  findset  16841  pw1ndom3  16890