Theorem simpr2 1068

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

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  simplr2  1104  simprr2  1110  simp1r2  1158  simp2r2  1164  simp3r2  1170  3anandis  1434  fpr2g  6475  isopolem  6595  fr3nr  6979  frfi  8205  intrnfi  8322  fisupcl  8375  cnfcomlem  8596  ackbij1lem15  9056  cofsmo  9091  sornom  9099  fpwwe2lem5  9456  dedekindle  10201  supmul1  10992  eluzuzle  11696  xlesubadd  12093  elioc2  12236  elico2  12237  elicc2  12238  fseq1p1m1  12414  fz0fzelfz0  12445  swrdsbslen  13448  swrdspsleq  13449  ccatswrd  13456  swrdswrdlem  13459  tanadd  14897  dvds2ln  15014  cshwsidrepsw  15800  ressress  15938  f1ovscpbl  16186  mreexexlem4d  16307  mreexexd  16308  mreexexdOLD  16309  iscatd2  16342  2oppccomf  16385  issubc3  16509  fthmon  16587  fuccocl  16624  fucidcl  16625  invfuc  16634  initoeu2lem0  16663  initoeu2lem1  16664  curf2cl  16871  yonedalem4c  16917  yonedalem3  16920  pospo  16973  latjle12  17062  latjlej1  17065  latnlej2  17071  latlem12  17078  latmlem1  17081  latledi  17089  latjass  17095  latj12  17096  latj32  17097  latj13  17098  latj31  17099  latjrot  17100  latjjdi  17103  latjjdir  17104  latdisdlem  17189  prdsmndd  17323  frmdmnd  17396  grpsubrcan  17496  grpsubadd  17503  grpaddsubass  17505  grpsubsub4  17508  grppnpcan2  17509  grpnpncan  17510  mulgnndir  17569  mulgnndirOLD  17570  mulgnn0dir  17571  mulgdir  17573  mulgnnass  17576  mulgnnassOLD  17577  mulgnn0ass  17578  mulgass  17579  mulgsubdir  17582  pwsmulg  17587  issubg2  17609  eqgval  17643  qusgrp  17649  galcan  17737  gacan  17738  oppgmnd  17784  symggrp  17820  fvcosymgeq  17849  pmtrprfv  17873  psgnunilem3  17916  cmn32  18211  cmn12  18213  abladdsub  18220  ablsubsub23  18230  mulgdi  18232  mulgsubdi  18235  dprdss  18428  dprdz  18429  dprdf1o  18431  dprdsn  18435  dprd2da  18441  dmdprdsplit  18446  ablfac1b  18469  pgpfac1lem5  18478  srgi  18511  srgbinom  18545  ringi  18560  prdsringd  18612  opprring  18631  mulgass3  18637  dvrass  18690  subrgunit  18798  issubrg2  18800  abvdiv  18837  lsssn0  18948  islss3  18959  prdslmodd  18969  islmhm2  19038  lspsolv  19143  islbs2  19154  islbs3  19155  lbsextlem4  19161  sralmod  19187  issubassa  19324  sraassa  19325  psrbaglesupp  19368  psrbaglecl  19369  psrbagcon  19371  psrgrp  19398  psrlmod  19401  psrring  19411  psrassa  19414  psgndiflemB  19946  ipdir  19984  ipdi  19985  ipsubdir  19987  ipsubdi  19988  ipass  19990  ipassr  19991  ipassr2  19992  isphld  19999  ocvlss  20016  mamudm  20194  matring  20249  matassa  20250  ofco2  20257  ma1repveval  20377  mdetunilem1  20418  mdetunilem9  20426  chpscmatgsumbin  20649  iinopn  20707  restopnb  20979  subbascn  21058  nrmsep2  21160  isnrm3  21163  regsep2  21180  dnsconst  21182  dfconn2  21222  1stcelcls  21264  dislly  21300  ptuni2  21379  tx1stc  21453  0nelfb  21635  infil  21667  fsubbas  21671  filssufilg  21715  hauspwpwf1  21791  cnextcn  21871  tmdcn2  21893  ustuqtoplem  22043  utopsnneiplem  22051  psmettri  22116  isxmet2d  22132  xmettri  22156  xmetres2  22166  bldisj  22203  blss2ps  22208  blss2  22209  xmstri2  22271  mstri2  22272  xmstri  22273  mstri  22274  xmstri3  22275  mstri3  22276  msrtri  22277  comet  22318  stdbdbl  22322  met2ndci  22327  ngprcan  22414  ngplcan  22415  ngpsubcan  22418  nmtri2  22431  nrgdsdi  22469  nrgdsdir  22470  nlmdsdi  22485  nlmdsdir  22486  blcvx  22601  icoopnst  22738  pi1grplem  22849  clmpm1dir  22903  cmodscmulexp  22922  cvsdiv  22932  cvsdivcl  22933  cphdivcl  22982  cphsubdir  23008  cphsubdi  23009  tchcph  23036  bcthlem5  23125  volfiniun  23315  volcn  23374  itg1val2  23451  dvconst  23680  dvlip  23756  ftc1a  23800  ulmval  24134  ulmdvlem3  24156  ang180  24544  cvxcl  24711  scvxcvx  24712  sgmmul  24926  dchrabl  24979  gausslemma2dlem1a  25090  motgrp  25438  iscgra1  25702  cgrane1  25704  cgrane3  25706  cgrahl1  25708  cgrahl2  25709  cgracgr  25710  cgratr  25715  cgrabtwn  25717  cgrahl  25718  dfcgra2  25721  sacgr  25722  f1otrge  25752  colinearalglem1  25786  axcgrtr  25795  axeuclidlem  25842  axcontlem3  25846  axcontlem4  25847  axcontlem7  25850  eengtrkg  25865  eengtrkge  25866  edglnl  26038  subgruhgredgd  26176  nbfusgrlevtxm2  26280  lfgriswlk  26585  umgrwwlks2on  26850  rusgrnumwwlks  26869  3spthd  27036  3vfriswmgr  27142  frgr2wwlkeqm  27195  numclwwlk2  27240  numclwwlk3OLD  27242  numclwwlk3  27243  numclwwlk5  27246  grpomuldivass  27395  ablomuldiv  27406  ablodivdiv4  27408  ablonnncan1  27412  nvmdi  27503  dipassr  27701  archiabllem2c  29749  dvrdir  29790  dvrcan5  29793  reofld  29840  pstmfval  29939  qqhval2lem  30025  qqhvq  30031  measdivcstOLD  30287  measdivcst  30288  carsggect  30380  tgoldbachgtd  30740  bnj1098  30854  bnj149  30945  bnj1118  31052  erdszelem9  31181  resconn  31228  cvmseu  31258  cvmlift2lem10  31294  cvmlift2lem12  31296  elmrsubrn  31417  mclsind  31467  frrlem4  31783  noprefixmo  31848  nosupbnd1  31860  ssltss2  31904  cgrid2  32110  segconeu  32118  btwncomim  32120  btwnswapid  32124  trisegint  32135  cgrxfr  32162  brofs2  32184  endofsegid  32192  btwnconn2  32209  seglemin  32220  segletr  32221  btwnsegle  32224  colinbtwnle  32225  broutsideof2  32229  btwnoutside  32232  broutsideof3  32233  outsideoftr  32236  outsidele  32239  fvray  32248  fvline  32251  ellines  32259  broucube  33443  ftc1anc  33493  sdclem1  33539  sstotbnd2  33573  iscringd  33797  lsmsat  34295  lfladdcl  34358  lflnegcl  34362  lflvscl  34364  eqlkr  34386  lshpkrlem4  34400  lshpkrlem6  34402  ldualgrplem  34432  lduallmodlem  34439  latmassOLD  34516  latm12  34517  latm32  34518  latmrot  34519  latmmdiN  34521  latmmdir  34522  omlfh1N  34545  omlfh3N  34546  cvrnbtwn2  34562  cvlexchb1  34617  cvlsupr2  34630  hlatjass  34656  hlatj12  34657  hlatj32  34658  cvrat  34708  cvrat2  34715  atltcvr  34721  atexchltN  34727  cvrat3  34728  cvrat4  34729  atbtwnexOLDN  34733  atbtwnex  34734  3dimlem3  34747  3dimlem3OLDN  34748  3at  34776  2atneat  34801  llncmp  34808  2at0mat0  34811  2atmat0  34812  llncvrlpln  34844  lplncmp  34848  2llnjaN  34852  4atlem11  34895  lplncvrlvol  34902  lvolcmp  34903  2atm2atN  35071  elpaddatriN  35089  paddasslem8  35113  paddass  35124  padd12N  35125  paddssw2  35130  paddss  35131  pmod1i  35134  pmodN  35136  pmapjlln1  35141  atmod1i1  35143  atmod1i2  35145  pexmidlem2N  35257  pl42lem2N  35266  pl42lem3N  35267  pl42lem4N  35268  pl42N  35269  lhpm0atN  35315  lautlt  35377  lautcvr  35378  lautj  35379  lautm  35380  ltrneq2  35434  cdlemd1  35485  cdleme1b  35513  cdleme1  35514  cdleme2  35515  cdleme3e  35519  cdlemefr27cl  35691  cdlemefs27cl  35701  cdleme42ke  35773  cdleme42mN  35775  cdlemf2  35850  cdlemftr2  35854  trljco  36028  tgrpgrplem  36037  tendoplass  36071  tendodi1  36072  tendodi2  36073  cdlemk34  36198  cdlemk36  36201  erngdvlem3-rN  36286  tendospdi1  36309  dialss  36335  dvhvaddass  36386  dvhopvsca  36391  dvhlveclem  36397  diblss  36459  diclss  36482  diclspsn  36483  cdlemn11pre  36499  dihmeetlem12N  36607  dihmeetlem16N  36611  dihmeetlem17N  36612  dihmeetlem18N  36613  dvh4dimN  36736  lpolconN  36776  dochpolN  36779  lclkr  36822  lclkrs  36828  lcfr  36874  irrapxlem6  37391  jm2.26lem3  37568  dgrsub2  37705  mpaaroot  37725  mendring  37762  mendlmod  37763  mendassa  37764  relexpmulg  38002  iunrelexpmin2  38004  relexpxpmin  38009  neicvgel1  38417  rfcnpre3  39192  fmuldfeq  39815  xlimbr  40053  stoweidlem43  40260  stoweidlem52  40269  stoweidlem53  40270  stoweidlem56  40273  stoweidlem57  40274  stoweidlem60  40277  issmfle  40954  issmfgt  40965  issmfge  40978  smflimlem4  40982  ltsubsubaddltsub  41315  iccpartigtl  41359  iccelpart  41369  upgrwlkupwlk  41721  copissgrp  41808  cznrng  41955  funcringcsetcALTV2lem9  42044  funcringcsetclem9ALTV  42067  ldepsprlem  42261  lincresunit3  42270  lincreslvec3  42271