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  5945  caovlem2d  6197  tfrlemibacc  6470  tfrlemibfn  6472  tfr1onlembacc  6486  tfr1onlembfn  6488  tfrcllembacc  6499  tfrcllembfn  6501  eqsupti  7159  prmuloc2  7750  ltntri  8270  elioc2  10128  elico2  10129  elicc2  10130  fseq1p1m1  10286  elfz0ubfz0  10317  ico0  10476  seq3f1olemp  10732  seq3f1oleml  10733  bcval5  10980  swrdsbslen  11193  ccatswrd  11197  isumss2  11899  tanaddap  12245  dvds2ln  12330  divalglemeunn  12427  divalglemex  12428  divalglemeuneg  12429  qredeq  12613  pcdvdstr  12845  isstructr  13042  prdssgrpd  13443  prdsmndd  13476  imasmnd2  13480  mndissubm  13503  grpsubrcan  13609  grpsubadd  13616  grpsubsub  13617  grpaddsubass  13618  grpsubsub4  13621  grpnnncan2  13625  imasgrp2  13642  mulgnndir  13683  mulgnn0dir  13684  mulgdir  13686  mulgnnass  13689  mulgnn0ass  13690  mulgass  13691  mulgsubdir  13694  issubg2m  13721  eqgval  13755  qusgrp  13764  kerf1ghm  13806  cmn32  13836  cmn12  13838  abladdsub  13847  rngass  13897  imasrng  13914  srgass  13929  ringdilem  13970  ringass  13974  imasring  14022  opprrng  14035  opprring  14037  mulgass3  14043  unitgrp  14074  dvrass  14097  dvrdir  14101  subrgunit  14197  issubrg2  14199  aprap  14244  islss3  14337  sralmod  14408  icnpimaex  14879  cnptopresti  14906  upxp  14940  psmettri  14998  isxmet2d  15016  xmettri  15040  metrtri  15045  xmetres2  15047  bldisj  15069  blss2ps  15074  blss2  15075  xmstri2  15138  mstri2  15139  xmstri  15140  mstri  15141  xmstri3  15142  mstri3  15143  msrtri  15144  comet  15167  bdbl  15171  xmetxp  15175  dvconst  15362  dvconstre  15364  dvconstss  15366  sgmmul  15664  findset  16266