Theorem simpr1 1027

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

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

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 1004

This theorem is referenced by:  simplr1  1063  simprr1  1069  simp1r1  1117  simp2r1  1123  simp3r1  1129  3anandis  1381  isopolem  5952  caovlem2d  6204  tfrlemibacc  6478  tfrlemibfn  6480  tfr1onlembacc  6494  tfr1onlembfn  6496  tfrcllembacc  6507  tfrcllembfn  6509  eqsupti  7174  prmuloc2  7765  ltntri  8285  elioc2  10144  elico2  10145  elicc2  10146  fseq1p1m1  10302  elfz0ubfz0  10333  ico0  10493  seq3f1olemp  10749  seq3f1oleml  10750  bcval5  10997  swrdsbslen  11213  ccatswrd  11217  isumss2  11919  tanaddap  12265  dvds2ln  12350  divalglemeunn  12447  divalglemex  12448  divalglemeuneg  12449  qredeq  12633  pcdvdstr  12865  isstructr  13062  prdssgrpd  13463  prdsmndd  13496  imasmnd2  13500  mndissubm  13523  grpsubrcan  13629  grpsubadd  13636  grpsubsub  13637  grpaddsubass  13638  grpsubsub4  13641  grpnnncan2  13645  imasgrp2  13662  mulgnndir  13703  mulgnn0dir  13704  mulgdir  13706  mulgnnass  13709  mulgnn0ass  13710  mulgass  13711  mulgsubdir  13714  issubg2m  13741  eqgval  13775  qusgrp  13784  kerf1ghm  13826  cmn32  13856  cmn12  13858  abladdsub  13867  rngass  13917  imasrng  13934  srgass  13949  ringdilem  13990  ringass  13994  imasring  14042  opprrng  14055  opprring  14057  mulgass3  14063  unitgrp  14095  dvrass  14118  dvrdir  14122  subrgunit  14218  issubrg2  14220  aprap  14265  islss3  14358  sralmod  14429  icnpimaex  14900  cnptopresti  14927  upxp  14961  psmettri  15019  isxmet2d  15037  xmettri  15061  metrtri  15066  xmetres2  15068  bldisj  15090  blss2ps  15095  blss2  15096  xmstri2  15159  mstri2  15160  xmstri  15161  mstri  15162  xmstri3  15163  mstri3  15164  msrtri  15165  comet  15188  bdbl  15192  xmetxp  15196  dvconst  15383  dvconstre  15385  dvconstss  15387  sgmmul  15685  findset  16363  pw1ndom3  16413