Theorem simpr2 1035

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

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

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 1011

This theorem is referenced by:  simplr2  1071  simprr2  1077  simp1r2  1125  simp2r2  1131  simp3r2  1137  3anandis  1388  isopolem  6018  tfrlemibacc  6587  tfrlemibfn  6589  tfr1onlembacc  6603  tfr1onlembfn  6605  tfrcllembacc  6616  tfrcllembfn  6618  prltlu  7844  prdisj  7849  prmuloc2  7924  ltntri  8444  eluzuzle  9909  xlesubadd  10264  elioc2  10317  elico2  10318  elicc2  10319  fseq1p1m1  10479  fz0fzelfz0  10512  seq3f1olemp  10930  bcval5  11179  hashdifpr  11239  hashtpgim  11275  swrdsbslen  11416  ccatswrd  11420  swrdswrdlem  11454  summodclem2  12127  isumss2  12138  tanaddap  12484  dvds2ln  12569  divalglemeunn  12666  divalglemex  12667  divalglemeuneg  12668  isstructr  13345  f1ovscpbl  13610  mndissubm  13759  grpsubrcan  13863  grpsubadd  13870  grpaddsubass  13872  grpsubsub4  13875  grppnpcan2  13876  grpnpncan  13877  mulgnndir  13931  mulgnn0dir  13932  mulgdir  13934  mulgnnass  13937  mulgnn0ass  13938  mulgass  13939  mulgsubdir  13942  issubg2m  13969  eqgval  14003  qusgrp  14012  cmn32  14084  cmn12  14086  abladdsub  14096  ablsubsub23  14106  prdssgrpd  14168  prdsmndd  14171  rngass  14213  srgdilem  14247  srgass  14249  ringdilem  14290  ringass  14294  opprrng  14355  opprring  14357  mulgass3  14364  unitgrp  14396  dvrass  14419  dvrdir  14423  subrgunit  14520  issubrg2  14522  aprap  14571  lsssn0  14679  islss3  14688  sralmod  14759  restopnb  15205  icnpimaex  15235  cnptopresti  15262  psmettri  15354  isxmet2d  15372  xmettri  15396  metrtri  15401  xmetres2  15403  bldisj  15425  blss2ps  15430  blss2  15431  xmstri2  15494  mstri2  15495  xmstri  15496  mstri  15497  xmstri3  15498  mstri3  15499  msrtri  15500  comet  15523  bdbl  15527  xmetxp  15531  dvconst  15718  dvconstre  15720  dvconstss  15722  sgmmul  16024  gausslemma2dlem1a  16091  pw1ndom3  16934