Theorem simpr2 1030

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 1024	. 2 |- ( ( ps /\ ch /\ th ) -> ch )
2	1	adantl 277	1 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1004

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 1006

This theorem is referenced by:  simplr2  1066  simprr2  1072  simp1r2  1120  simp2r2  1126  simp3r2  1132  3anandis  1383  isopolem  5962  tfrlemibacc  6491  tfrlemibfn  6493  tfr1onlembacc  6507  tfr1onlembfn  6509  tfrcllembacc  6520  tfrcllembfn  6522  prltlu  7706  prdisj  7711  prmuloc2  7786  ltntri  8306  eluzuzle  9763  xlesubadd  10117  elioc2  10170  elico2  10171  elicc2  10172  fseq1p1m1  10328  fz0fzelfz0  10361  seq3f1olemp  10776  bcval5  11024  hashdifpr  11083  swrdsbslen  11246  ccatswrd  11250  swrdswrdlem  11284  summodclem2  11942  isumss2  11953  tanaddap  12299  dvds2ln  12384  divalglemeunn  12481  divalglemex  12482  divalglemeuneg  12483  isstructr  13096  f1ovscpbl  13394  prdssgrpd  13497  prdsmndd  13530  mndissubm  13557  grpsubrcan  13663  grpsubadd  13670  grpaddsubass  13672  grpsubsub4  13675  grppnpcan2  13676  grpnpncan  13677  mulgnndir  13737  mulgnn0dir  13738  mulgdir  13740  mulgnnass  13743  mulgnn0ass  13744  mulgass  13745  mulgsubdir  13748  issubg2m  13775  eqgval  13809  qusgrp  13818  cmn32  13890  cmn12  13892  abladdsub  13901  ablsubsub23  13911  rngass  13951  srgdilem  13981  srgass  13983  ringdilem  14024  ringass  14028  opprrng  14089  opprring  14091  mulgass3  14097  unitgrp  14129  dvrass  14152  dvrdir  14156  subrgunit  14252  issubrg2  14254  aprap  14299  lsssn0  14383  islss3  14392  sralmod  14463  restopnb  14904  icnpimaex  14934  cnptopresti  14961  psmettri  15053  isxmet2d  15071  xmettri  15095  metrtri  15100  xmetres2  15102  bldisj  15124  blss2ps  15129  blss2  15130  xmstri2  15193  mstri2  15194  xmstri  15195  mstri  15196  xmstri3  15197  mstri3  15198  msrtri  15199  comet  15222  bdbl  15226  xmetxp  15230  dvconst  15417  dvconstre  15419  dvconstss  15421  sgmmul  15719  gausslemma2dlem1a  15786  pw1ndom3  16589