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  5958  tfrlemibacc  6487  tfrlemibfn  6489  tfr1onlembacc  6503  tfr1onlembfn  6505  tfrcllembacc  6516  tfrcllembfn  6518  prltlu  7697  prdisj  7702  prmuloc2  7777  ltntri  8297  eluzuzle  9754  xlesubadd  10108  elioc2  10161  elico2  10162  elicc2  10163  fseq1p1m1  10319  fz0fzelfz0  10352  seq3f1olemp  10767  bcval5  11015  hashdifpr  11074  swrdsbslen  11237  ccatswrd  11241  swrdswrdlem  11275  summodclem2  11933  isumss2  11944  tanaddap  12290  dvds2ln  12375  divalglemeunn  12472  divalglemex  12473  divalglemeuneg  12474  isstructr  13087  f1ovscpbl  13385  prdssgrpd  13488  prdsmndd  13521  mndissubm  13548  grpsubrcan  13654  grpsubadd  13661  grpaddsubass  13663  grpsubsub4  13666  grppnpcan2  13667  grpnpncan  13668  mulgnndir  13728  mulgnn0dir  13729  mulgdir  13731  mulgnnass  13734  mulgnn0ass  13735  mulgass  13736  mulgsubdir  13739  issubg2m  13766  eqgval  13800  qusgrp  13809  cmn32  13881  cmn12  13883  abladdsub  13892  ablsubsub23  13902  rngass  13942  srgdilem  13972  srgass  13974  ringdilem  14015  ringass  14019  opprrng  14080  opprring  14082  mulgass3  14088  unitgrp  14120  dvrass  14143  dvrdir  14147  subrgunit  14243  issubrg2  14245  aprap  14290  lsssn0  14374  islss3  14383  sralmod  14454  restopnb  14895  icnpimaex  14925  cnptopresti  14952  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  gausslemma2dlem1a  15777  pw1ndom3  16525