Theorem simpr2 1028

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpr2	|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ch )

Proof of Theorem simpr2

Step	Hyp	Ref	Expression
1		simp2 1022	. 2 |- ( ( ps /\ ch /\ th ) -> ch )
2	1	adantl 277	1 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ch )

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:  simplr2  1064  simprr2  1070  simp1r2  1118  simp2r2  1124  simp3r2  1130  3anandis  1381  isopolem  5945  tfrlemibacc  6470  tfrlemibfn  6472  tfr1onlembacc  6486  tfr1onlembfn  6488  tfrcllembacc  6499  tfrcllembfn  6501  prltlu  7670  prdisj  7675  prmuloc2  7750  ltntri  8270  eluzuzle  9726  xlesubadd  10075  elioc2  10128  elico2  10129  elicc2  10130  fseq1p1m1  10286  fz0fzelfz0  10319  seq3f1olemp  10732  bcval5  10980  hashdifpr  11037  swrdsbslen  11193  ccatswrd  11197  swrdswrdlem  11231  summodclem2  11888  isumss2  11899  tanaddap  12245  dvds2ln  12330  divalglemeunn  12427  divalglemex  12428  divalglemeuneg  12429  isstructr  13042  f1ovscpbl  13340  prdssgrpd  13443  prdsmndd  13476  mndissubm  13503  grpsubrcan  13609  grpsubadd  13616  grpaddsubass  13618  grpsubsub4  13621  grppnpcan2  13622  grpnpncan  13623  mulgnndir  13683  mulgnn0dir  13684  mulgdir  13686  mulgnnass  13689  mulgnn0ass  13690  mulgass  13691  mulgsubdir  13694  issubg2m  13721  eqgval  13755  qusgrp  13764  cmn32  13836  cmn12  13838  abladdsub  13847  ablsubsub23  13857  rngass  13897  srgdilem  13927  srgass  13929  ringdilem  13970  ringass  13974  opprrng  14035  opprring  14037  mulgass3  14043  unitgrp  14074  dvrass  14097  dvrdir  14101  subrgunit  14197  issubrg2  14199  aprap  14244  lsssn0  14328  islss3  14337  sralmod  14408  restopnb  14849  icnpimaex  14879  cnptopresti  14906  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  gausslemma2dlem1a  15731