Theorem simpr1 1067

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpr1	|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ps )

Proof of Theorem simpr1

Step	Hyp	Ref	Expression
1		simp1 1061	. 2 |- ( ( ps /\ ch /\ th ) -> ps )
2	1	adantl 482	1 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ps )

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:  simplr1  1103  simprr1  1109  simp1r1  1157  simp2r1  1163  simp3r1  1169  3anandis  1434  fpr2g  6475  isopolem  6595  fr3nr  6979  suppfnss  7320  frfi  8205  intrnfi  8322  iinfi  8323  eqsup  8362  fisupcl  8375  cnfcomlem  8596  ackbij1lem15  9056  fpwwe2lem5  9456  dedekindle  10201  ico0  12221  elioc2  12236  elico2  12237  elicc2  12238  iccsplit  12305  fseq1p1m1  12414  elfz0ubfz0  12443  hashtpg  13267  swrdsbslen  13448  swrdspsleq  13449  ccatswrd  13456  tanadd  14897  dvds2ln  15014  qredeq  15371  ressress  15938  mreexexlem4d  16307  mreexexd  16308  mreexexdOLD  16309  0catg  16348  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  latmlej11  17090  latjass  17095  latj12  17096  latj32  17097  latj13  17098  latj31  17099  latjrot  17100  latjjdi  17103  latjjdir  17104  latdisdlem  17189  prdsmndd  17323  imasmnd2  17327  frmdmnd  17396  grpsubrcan  17496  grpsubadd  17503  grpsubsub  17504  grpaddsubass  17505  grpsubsub4  17508  grpnnncan2  17512  imasgrp2  17530  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  pmtrprfv  17873  pmtr3ncom  17895  psgnunilem3  17916  cmn32  18211  cmn12  18213  abladdsub  18220  mulgnn0di  18231  mulgdi  18232  mulgsubdi  18235  dprdss  18428  dprdz  18429  dprdf1o  18431  dprdsn  18435  dprd2da  18441  ablfac1b  18469  pgpfac1lem5  18478  srgbinomlem2  18541  srgbinom  18545  ringi  18560  prdsringd  18612  imasring  18619  opprring  18631  mulgass3  18637  dvrass  18690  kerf1hrm  18743  subrgunit  18798  issubrg2  18800  abvdiv  18837  islss3  18959  prdslmodd  18969  islmhm2  19038  lspsolv  19143  islbs2  19154  islbs3  19155  lbsextlem4  19161  sralmod  19187  issubassa  19324  sraassa  19325  psrbaglecl  19369  psrbagcon  19371  psrgrp  19398  psrlmod  19401  psrring  19411  psrassa  19414  ipdir  19984  ipdi  19985  ipsubdir  19987  ipsubdi  19988  ipass  19990  ipassr  19991  ipassr2  19992  ocvlss  20016  mamudm  20194  matring  20249  matassa  20250  ofco2  20257  mdetunilem1  20418  mdetunilem9  20426  mdetuni0  20427  mdetmul  20429  gsummatr01lem3  20463  iinopn  20707  subbascn  21058  nrmsep2  21160  isnrm3  21163  regsep2  21180  dnsconst  21182  dfconn2  21222  1stcelcls  21264  nllyidm  21292  dislly  21300  upxp  21426  fbasne0  21634  filss  21657  infil  21667  fsubbas  21671  filssufilg  21715  tmdcn2  21893  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  icccmplem2  22626  pi1grplem  22849  pi1cof  22859  clmpm1dir  22903  cvsdiv  22932  cvsdivcl  22933  cphdivcl  22982  cphsubdir  23008  cphsubdi  23009  cphassr  23012  bcthlem5  23125  rrxcph  23180  volfiniun  23315  volcn  23374  itg1val2  23451  dvconst  23680  dvlip  23756  dvfsumlem4  23792  ftc1a  23800  ulmval  24134  ulmdvlem3  24156  ang180  24544  cvxcl  24711  scvxcvx  24712  sgmmul  24926  logexprlim  24950  dchrabl  24979  motgrp  25438  iscgra1  25702  cgrane1  25704  cgrane2  25705  cgrahl1  25708  cgrahl2  25709  cgracgr  25710  cgratr  25715  cgrabtwn  25717  dfcgra2  25721  sacgr  25722  f1otrge  25752  colinearalglem1  25786  colinearalg  25790  axcgrtr  25795  axlowdimlem16  25837  axeuclidlem  25842  axcontlem7  25850  eengtrkg  25865  eengtrkge  25866  nbfusgrlevtxm2  26280  lfgriswlk  26585  upgrwlkdvde  26633  erclwwlkstr  26936  erclwwlksntr  26948  frgr2wwlkeqm  27195  numclwwlk5  27246  friendship  27257  grpodivdiv  27394  grpomuldivass  27395  ablodivdiv4  27408  ablonnncan  27410  ablonnncan1  27412  nvmdi  27503  dipassr  27701  archiabllem2c  29749  dvrdir  29790  dvrcan5  29793  reofld  29840  pstmfval  29939  tpr2rico  29958  qqhval2lem  30025  qqhvq  30031  issiga  30174  measdivcstOLD  30287  measdivcst  30288  carsggect  30380  signsply0  30628  tgoldbachgtd  30740  bnj149  30945  bnj1118  31052  bnj1128  31058  erdszelem9  31181  resconn  31228  cvmseu  31258  cvmlift2lem12  31296  elmrsubrn  31417  mclsind  31467  noprefixmo  31848  nosupbnd1  31860  ssltss1  31903  cgrid2  32110  segconeu  32118  btwncomim  32120  btwnswapid  32124  cgrxfr  32162  btwnxfr  32163  colineardim1  32168  brofs2  32184  brifs2  32185  idinside  32191  endofsegid  32192  btwnconn1lem7  32200  btwnconn1lem11  32204  btwnconn1  32208  segcon2  32212  seglemin  32220  segletr  32221  btwnsegle  32224  colinbtwnle  32225  broutsideof2  32229  broutsideof3  32233  outsidele  32239  fvray  32248  fvline  32251  linerflx1  32256  ellines  32259  ivthALT  32330  poimirlem32  33441  ftc1anc  33493  sdclem1  33539  sstotbnd2  33573  zerdivemp1x  33746  isdrngo2  33757  iscringd  33797  lsmsat  34295  lfladdcl  34358  lflnegcl  34362  lflvscl  34364  lshpkrlem4  34400  lshpkrlem6  34402  ldualgrplem  34432  lduallmodlem  34439  latmassOLD  34516  latm12  34517  latm32  34518  latmrot  34519  latmmdiN  34521  latmmdir  34522  omlfh1N  34545  omlfh3N  34546  cvlexchb1  34617  cvlexch3  34619  cvlexch4N  34620  cvlatexchb1  34621  cvlsupr2  34630  hlatjass  34656  hlatj12  34657  hlatj32  34658  cvratlem  34707  cvrat  34708  atcvrj0  34714  cvrat2  34715  atltcvr  34721  atexchltN  34727  cvrat3  34728  cvrat4  34729  3dimlem3  34747  3dimlem3OLDN  34748  3at  34776  2atneat  34801  llncmp  34808  2at0mat0  34811  2atmat0  34812  lplnnle2at  34827  llncvrlpln  34844  lplncmp  34848  lplnexllnN  34850  2llnjaN  34852  4atlem11  34895  lplncvrlvol  34902  lvolcmp  34903  2atm2atN  35071  elpaddatriN  35089  paddasslem9  35114  paddass  35124  padd12N  35125  paddssw2  35130  paddss  35131  pmodlem2  35133  pmodN  35136  pmapjlln1  35141  atmod1i1  35143  atmod1i2  35145  pexmidlem2N  35257  pexmidlem6N  35261  pl42N  35269  lhpm0atN  35315  lautlt  35377  lautcvr  35378  lautj  35379  lautm  35380  ltrneq2  35434  cdlemc3  35480  cdlemc4  35481  cdlemd1  35485  cdleme1b  35513  cdleme1  35514  cdleme2  35515  cdleme3e  35519  cdlemefr27cl  35691  cdlemefs27cl  35701  cdleme42mN  35775  cdlemftr2  35854  trljco  36028  tgrpgrplem  36037  tendoplass  36071  tendodi1  36072  tendodi2  36073  cdlemk36  36201  erngdvlem3  36278  erngdvlem3-rN  36286  tendospdi1  36309  dvalveclem  36314  dialss  36335  dvhvaddass  36386  dvhopvsca  36391  dvhlveclem  36397  diblss  36459  diclss  36482  dihmeetlem12N  36607  dihmeetlem15N  36610  dihmeetlem16N  36611  dihmeetlem17N  36612  dihmeetlem18N  36613  dihmeetlem19N  36614  dvh4dimN  36736  lpolvN  36775  lclkr  36822  lclkrs  36828  lcfr  36874  irrapxlem6  37391  jm2.26lem3  37568  dgrsub2  37705  mpaadgr  37724  mendring  37762  mendlmod  37763  mendassa  37764  relexpmulg  38002  iunrelexpmin2  38004  relexpxpmin  38009  neicvgel1  38417  fmuldfeq  39815  stoweidlem43  40260  stoweidlem52  40269  stoweidlem53  40270  stoweidlem56  40273  stoweidlem57  40274  issmfle  40954  issmfgt  40965  issmfge  40978  fmtnoprmfac1  41477  fmtnoprmfac2  41479  upgrwlkupwlk  41721  copissgrp  41808  cznrng  41955  funcringcsetcALTV2lem9  42044  funcringcsetclem9ALTV  42067  ply1ass23l  42170  linccl  42203  lincext1  42243  lincext3  42245  lincresunit2  42267