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  5952  tfrlemibacc  6478  tfrlemibfn  6480  tfr1onlembacc  6494  tfr1onlembfn  6496  tfrcllembacc  6507  tfrcllembfn  6509  prltlu  7685  prdisj  7690  prmuloc2  7765  ltntri  8285  eluzuzle  9742  xlesubadd  10091  elioc2  10144  elico2  10145  elicc2  10146  fseq1p1m1  10302  fz0fzelfz0  10335  seq3f1olemp  10749  bcval5  10997  hashdifpr  11055  swrdsbslen  11213  ccatswrd  11217  swrdswrdlem  11251  summodclem2  11908  isumss2  11919  tanaddap  12265  dvds2ln  12350  divalglemeunn  12447  divalglemex  12448  divalglemeuneg  12449  isstructr  13062  f1ovscpbl  13360  prdssgrpd  13463  prdsmndd  13496  mndissubm  13523  grpsubrcan  13629  grpsubadd  13636  grpaddsubass  13638  grpsubsub4  13641  grppnpcan2  13642  grpnpncan  13643  mulgnndir  13703  mulgnn0dir  13704  mulgdir  13706  mulgnnass  13709  mulgnn0ass  13710  mulgass  13711  mulgsubdir  13714  issubg2m  13741  eqgval  13775  qusgrp  13784  cmn32  13856  cmn12  13858  abladdsub  13867  ablsubsub23  13877  rngass  13917  srgdilem  13947  srgass  13949  ringdilem  13990  ringass  13994  opprrng  14055  opprring  14057  mulgass3  14063  unitgrp  14095  dvrass  14118  dvrdir  14122  subrgunit  14218  issubrg2  14220  aprap  14265  lsssn0  14349  islss3  14358  sralmod  14429  restopnb  14870  icnpimaex  14900  cnptopresti  14927  psmettri  15019  isxmet2d  15037  xmettri  15061  metrtri  15066  xmetres2  15068  bldisj  15090  blss2ps  15095  blss2  15096  xmstri2  15159  mstri2  15160  xmstri  15161  mstri  15162  xmstri3  15163  mstri3  15164  msrtri  15165  comet  15188  bdbl  15192  xmetxp  15196  dvconst  15383  dvconstre  15385  dvconstss  15387  sgmmul  15685  gausslemma2dlem1a  15752  pw1ndom3  16413