Theorem simpr1 1029

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

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

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 1006

This theorem is referenced by:  simplr1  1065  simprr1  1071  simp1r1  1119  simp2r1  1125  simp3r1  1131  3anandis  1383  isopolem  5962  caovlem2d  6214  tfrlemibacc  6491  tfrlemibfn  6493  tfr1onlembacc  6507  tfr1onlembfn  6509  tfrcllembacc  6520  tfrcllembfn  6522  eqsupti  7194  prmuloc2  7786  ltntri  8306  elioc2  10170  elico2  10171  elicc2  10172  fseq1p1m1  10328  elfz0ubfz0  10359  ico0  10520  seq3f1olemp  10776  seq3f1oleml  10777  bcval5  11024  swrdsbslen  11246  ccatswrd  11250  isumss2  11953  tanaddap  12299  dvds2ln  12384  divalglemeunn  12481  divalglemex  12482  divalglemeuneg  12483  qredeq  12667  pcdvdstr  12899  isstructr  13096  prdssgrpd  13497  prdsmndd  13530  imasmnd2  13534  mndissubm  13557  grpsubrcan  13663  grpsubadd  13670  grpsubsub  13671  grpaddsubass  13672  grpsubsub4  13675  grpnnncan2  13679  imasgrp2  13696  mulgnndir  13737  mulgnn0dir  13738  mulgdir  13740  mulgnnass  13743  mulgnn0ass  13744  mulgass  13745  mulgsubdir  13748  issubg2m  13775  eqgval  13809  qusgrp  13818  kerf1ghm  13860  cmn32  13890  cmn12  13892  abladdsub  13901  rngass  13951  imasrng  13968  srgass  13983  ringdilem  14024  ringass  14028  imasring  14076  opprrng  14089  opprring  14091  mulgass3  14097  unitgrp  14129  dvrass  14152  dvrdir  14156  subrgunit  14252  issubrg2  14254  aprap  14299  islss3  14392  sralmod  14463  icnpimaex  14934  cnptopresti  14961  upxp  14995  psmettri  15053  isxmet2d  15071  xmettri  15095  metrtri  15100  xmetres2  15102  bldisj  15124  blss2ps  15129  blss2  15130  xmstri2  15193  mstri2  15194  xmstri  15195  mstri  15196  xmstri3  15197  mstri3  15198  msrtri  15199  comet  15222  bdbl  15226  xmetxp  15230  dvconst  15417  dvconstre  15419  dvconstss  15421  sgmmul  15719  findset  16540  pw1ndom3  16589