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  5958  caovlem2d  6210  tfrlemibacc  6487  tfrlemibfn  6489  tfr1onlembacc  6503  tfr1onlembfn  6505  tfrcllembacc  6516  tfrcllembfn  6518  eqsupti  7186  prmuloc2  7777  ltntri  8297  elioc2  10161  elico2  10162  elicc2  10163  fseq1p1m1  10319  elfz0ubfz0  10350  ico0  10511  seq3f1olemp  10767  seq3f1oleml  10768  bcval5  11015  swrdsbslen  11237  ccatswrd  11241  isumss2  11944  tanaddap  12290  dvds2ln  12375  divalglemeunn  12472  divalglemex  12473  divalglemeuneg  12474  qredeq  12658  pcdvdstr  12890  isstructr  13087  prdssgrpd  13488  prdsmndd  13521  imasmnd2  13525  mndissubm  13548  grpsubrcan  13654  grpsubadd  13661  grpsubsub  13662  grpaddsubass  13663  grpsubsub4  13666  grpnnncan2  13670  imasgrp2  13687  mulgnndir  13728  mulgnn0dir  13729  mulgdir  13731  mulgnnass  13734  mulgnn0ass  13735  mulgass  13736  mulgsubdir  13739  issubg2m  13766  eqgval  13800  qusgrp  13809  kerf1ghm  13851  cmn32  13881  cmn12  13883  abladdsub  13892  rngass  13942  imasrng  13959  srgass  13974  ringdilem  14015  ringass  14019  imasring  14067  opprrng  14080  opprring  14082  mulgass3  14088  unitgrp  14120  dvrass  14143  dvrdir  14147  subrgunit  14243  issubrg2  14245  aprap  14290  islss3  14383  sralmod  14454  icnpimaex  14925  cnptopresti  14952  upxp  14986  psmettri  15044  isxmet2d  15062  xmettri  15086  metrtri  15091  xmetres2  15093  bldisj  15115  blss2ps  15120  blss2  15121  xmstri2  15184  mstri2  15185  xmstri  15186  mstri  15187  xmstri3  15188  mstri3  15189  msrtri  15190  comet  15213  bdbl  15217  xmetxp  15221  dvconst  15408  dvconstre  15410  dvconstss  15412  sgmmul  15710  findset  16476  pw1ndom3  16525