Theorem simpl1 999

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

Assertion

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

Proof of Theorem simpl1

Step	Hyp	Ref	Expression
1		simp1 996	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2	1	adantr 465	1 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 973

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 185  df-an 371  df-3an 975

This theorem is referenced by:  simpll1  1035  simprl1  1041  simp1l1  1089  simp2l1  1095  simp3l1  1101  3anandirs  1331  rspc3ev  3227  brcogw  5171  cocan1  6182  weniso  6238  smogt  7038  smorndom  7039  omeulem1  7231  nnmord  7281  nnmword  7282  difsnen  7599  enfixsn  7626  mapunen  7686  ac6sfi  7764  fipreima  7826  elfiun  7890  ordiso2  7940  wemaplem2  7972  wemapso  7976  en2eqpr  8385  indcardi  8422  fodomfi2  8441  iunfictbso  8495  infmap2  8598  cofsmo  8649  cfsmolem  8650  coftr  8653  fin23lem11  8697  fincssdom  8703  fin23lem26  8705  isf32lem9  8741  ac6num  8859  gchdomtri  9007  gchpwdom  9048  winainflem  9071  tskuni  9161  gruima  9180  gruf  9189  grudomon  9195  elnpi  9366  distrlem4pr  9404  prlem934  9411  addcan  9763  addcan2  9764  ltmul1a  10391  ledivmulOLD  10419  ledivmul2OLD  10423  suprleub  10507  supmul1  10508  infmrgelb  10523  suprzcl  10940  uzsupss  11174  xleadd1a  11445  xlesubadd  11455  xmulasslem3  11478  xlemul2a  11481  xadddilem  11486  xadddi2  11489  ixxun  11545  icoshftf1o  11643  snunioc  11648  lincmb01cmp  11663  iccf1o  11664  fzofzim  11837  ltexp2a  12185  leexp2  12188  ltexp2r  12190  exple1  12193  expnlbnd2  12265  ccatass  12570  swrdswrdlem  12647  ccatopth  12658  cshco  12765  repsco  12768  s2f1o  12827  limsupgre  13267  addcn2  13379  mulcn2  13381  dvdsadd2b  13887  dvdsmod  13902  oexpneg  13908  gcdass  14042  rplpwr  14053  rppwr  14054  coprmdvds2  14103  rpmulgcd2  14105  qredeq  14106  rpexp  14120  rpdvds  14124  prmdiveq  14175  odzdvds  14181  modprmn0modprm0  14191  coprimeprodsq2  14193  pythagtriplem3  14201  pcdvdsb  14251  pcgcd1  14259  qexpz  14279  pockthg  14283  vdwnnlem1  14372  0ram  14397  ramz2  14401  lubss  15608  lubun  15610  clatleglb  15613  clatglbss  15614  mrelatglb  15671  issubmnd  15767  ress0g  15768  gsumccat  15841  frmdss2  15863  mulgneg  15970  mulgdirlem  15976  submmulg  15987  subgmulg  16020  nmzsubg  16047  ghmmulg  16084  gsmsymgreqlem1  16260  pmtrfb  16296  psgnunilem4  16328  odmodnn0  16370  odnncl  16375  odmod  16376  odmulgid  16382  odmulgeq  16385  odf1o1  16398  odf1o2  16399  odngen  16403  gexdvdsi  16409  pgpfi1  16421  odcau  16430  subgslw  16442  fislw  16451  lsmssv  16469  lsmless1x  16470  lsmless2x  16471  lsmsubm  16479  lsmmod  16499  lsmmod2  16500  efgred  16572  cntzcmn  16651  ghmplusg  16655  odadd1  16657  odadd2  16658  odadd  16659  lsmcomx  16665  gsumconst  16757  rng1eq0  17039  mulgass2  17048  isabvd  17269  lssintcl  17410  0lmhm  17486  lmhmvsca  17491  reslmhm2b  17500  pwssplit1  17505  pwssplit3  17507  lspfixed  17574  lspsnat  17591  lidldvgen  17702  issubassa  17772  evlsval2  17988  psrplusgpropd  18076  coe1subfv  18106  coe1mul2  18109  xrsdsreclblem  18260  regsumsupp  18453  obselocv  18554  uvcresum  18619  frlmsslsp  18624  frlmsslspOLD  18625  frlmup4  18630  lindff1  18650  f1lindf  18652  lsslindf  18660  islindf4  18668  lbslcic  18671  mhmvlin  18694  mamutpos  18755  scmatscmide  18804  mavmulsolcl  18848  marrepcl  18861  mdetdiag  18896  mdetunilem1  18909  mdetunilem3  18911  mdetunilem7  18915  mdetunilem9  18917  mdetmul  18920  slesolinvbi  18978  m2pmfzmap  19043  pmatcollpwlem  19076  pmatcollpw  19077  mp2pm2mplem4  19105  chpdmatlem3  19136  chfacfisfcpmat  19151  chfacfscmulgsum  19156  chfacfpmmulgsum  19160  chfacfpmmulgsum2  19161  cayhamlem1  19162  cpmidpmatlem2  19167  cpmadugsumlemB  19170  cpmadugsumlemC  19171  cpmadugsumlemF  19172  riinopn  19212  neiint  19399  topssnei  19419  restntr  19477  iscnp4  19558  cnconst2  19578  cnrest2  19581  cnprest2  19585  cnpdis  19588  cnt0  19641  cnt1  19645  cnhaus  19649  ordthauslem  19678  cncmp  19686  fiuncmp  19698  sscmp  19699  hauscmp  19701  cnconn  19717  uncon  19724  nlly2i  19771  llynlly  19772  nllyidm  19784  ptrescn  19903  xkococnlem  19923  qtoptop2  19963  qtopss  19979  kqfvima  19994  r0cld  20002  ordthmeolem  20065  fbssint  20102  fmf  20209  fmss  20210  elfm  20211  rnelfmlem  20216  rnelfm  20217  fmco  20225  flimss2  20236  flimss1  20237  flimrest  20247  flftg  20260  cnpflf2  20264  cnpflf  20265  flfcnp  20268  supnfcls  20284  fclsss1  20286  fclsss2  20287  fcfnei  20299  fcfelbas  20300  cnpfcfi  20304  subgntr  20368  opnsubg  20369  cldsubg  20372  ghmcnp  20376  utop2nei  20516  neipcfilu  20562  bldisj  20664  blgt0  20665  bl2in  20666  blss2ps  20669  blss2  20670  blssps  20690  blss  20691  xmetresbl  20703  lpbl  20769  blcld  20771  stdbdbl  20783  metcnp3  20806  metcnp2  20808  txmetcnp  20813  blval2  20841  nmoix  20999  nmoeq0  21006  icoopnst  21202  iocopnst  21203  xrhmeo  21209  nmhmcn  21366  cphsqrtcl2  21396  cphsqrtcl3  21397  cfil3i  21471  caublcls  21510  bcthlem5  21530  cmetcusp1OLD  21554  cmetcusp1  21555  rrxcph  21587  pjth  21617  ovoliunlem2  21677  volun  21718  volsup2  21777  mbfimaopn2  21827  iblconst  21987  itgconst  21988  dvcnp2  22086  dvcn  22087  deg1mul3le  22280  deg1tmle  22281  dvdsq1p  22324  ig1peu  22335  ig1pdvds  22340  coeid3  22400  dgrmulc  22430  efcvx  22606  tanord  22686  logdivlti  22761  logccv  22800  recxpcl  22812  cxpeq  22887  ang180  22902  isosctrlem2  22909  cxp2lim  23062  amgm  23076  muval1  23163  dvdssqf  23168  mumullem2  23210  mumul  23211  bcmono  23308  lgsfcl2  23333  lgsdilem  23353  lgsdirprm  23360  lgsdir  23361  lgsdi  23363  lgsne0  23364  brbtwn2  23912  colinearalglem1  23913  colinearalg  23917  axcgrtr  23922  axsegconlem8  23931  axsegconlem9  23932  axsegconlem10  23933  axcontlem8  23978  axcontlem10  23980  2pthon  24308  clwwlkfo  24501  clwwlkext2edg  24506  erclwwlksym  24518  erclwwlknsym  24530  clwlkfoclwwlk  24549  clwlkf1clwwlklem  24553  numclwwlk2lem1  24807  numclwwlk5  24817  frgraregord13  24824  gxcom  24975  gxnn0add  24980  zerdivemp1  25140  nvmul0or  25251  ipval2lem2  25318  ipval2lem5  25324  lnomul  25379  shless  25981  shlej1  25982  pjspansn  26199  hoadddi  26426  kbmul  26578  homco2  26600  kbass2  26740  eliccelico  27284  elicoelioo  27285  iocinioc2  27286  iocinif  27288  xrge0adddir  27372  xrge0npcan  27374  archiabl  27432  ress1r  27470  rhmdvdsr  27499  pstmfval  27539  fmcncfil  27577  zrhnm  27614  qqhnm  27635  measvunilem  27851  volfiniune  27870  dya2iocnrect  27920  sibfinima  27949  probun  28026  probinc  28028  cndprob01  28042  signswmnd  28182  pconpi1  28350  cvmsss2  28387  ntrivcvgmul  28641  binomrisefac  28769  dvdspw  28780  br6  28791  br4  28792  frrlem4  28995  cgrcomim  29244  cgrtriv  29257  cgrextend  29263  segconeq  29265  btwntriv2  29267  btwnintr  29274  btwnexch3  29275  btwnouttr2  29277  trisegint  29283  cgrsub  29300  cgrxfr  29310  btwnxfr  29311  lineext  29331  btwnconn1lem13  29354  btwnconn1lem14  29355  btwnconn3  29358  segcon2  29360  brsegle  29363  brsegle2  29364  segletr  29369  segleantisym  29370  seglelin  29371  outsideofeu  29386  lineunray  29402  lineelsb2  29403  areacirc  29717  ivthALT  29758  finlocfin  29799  cocanfo  29839  upixp  29851  ismtyima  29930  rrndstprj2  29958  zerdivemp1x  29989  mzprename  30314  eldioph2lem1  30325  lzunuz  30333  rencldnfi  30387  pellexlem2  30398  infmrgelbi  30446  pellfundglb  30453  pellfund14gap  30455  qirropth  30476  rmxycomplete  30485  congadd  30536  acongeq  30553  jm2.19  30567  jm2.23  30570  jm2.20nn  30571  jm2.27  30582  jm3.1  30594  aomclem6  30637  lnmepi  30663  lmhmfgsplit  30664  lmhmlnmsplit  30665  pwssplit4  30667  hbtlem2  30705  hbtlem5  30709  dgraa0p  30731  hashgcdlem  30790  proot1hash  30793  iocunico  30811  lcmass  30846  suprnmpt  31057  snunioo2  31136  snunioo1  31144  iccintsng  31155  lptre2pt  31210  limcleqr  31214  volioc  31318  iblspltprt  31319  stoweidlem19  31347  stoweidlem20  31348  stoweidlem22  31350  stoweidlem28  31356  stoweidlem34  31362  stoweidlem44  31372  stoweidlem60  31388  wallispilem3  31395  fourierdlem41  31476  fourierdlem42  31477  fourierdlem49  31484  fourierdlem51  31486  fourierdlem54  31489  fourierdlem74  31509  fourierdlem97  31532  fzoopth  31835  ofaddmndmap  32029  lincdifsn  32124  lincellss  32126  lincresunit3lem3  32174  islindeps2  32183  lindssnlvec  32186  bnj517  33040  bnj594  33067  lsatfixedN  33824  lssat  33831  eqlkr  33914  eqlkr2  33915  lkrlsp  33917  lshpkrlem4  33928  opposet  33996  cvrcon3b  34092  cvrcmp  34098  atlen0  34125  atnle  34132  atlatmstc  34134  cvlatexch3  34153  cvlsupr2  34158  hlsupr2  34201  hlrelat2  34217  cvrexchlem  34233  lnnat  34241  atcvrj2b  34246  atle  34250  atexchcvrN  34254  atbtwn  34260  athgt  34270  3dimlem3  34275  3dim1  34281  1cvratlt  34288  1cvrjat  34289  ps-1  34291  ps-2  34292  3atlem3  34299  3atlem5  34301  3atlem7  34303  llni  34322  llni2  34326  atcvrlln2  34333  llnexatN  34335  llncmp  34336  2llnmat  34338  2at0mat0  34339  lplni  34346  lplnnle2at  34355  2atnelpln  34358  lplnllnneN  34370  llncvrlpln2  34371  2lplnmN  34373  2llnmj  34374  lplncmp  34376  lplnexatN  34377  lplnexllnN  34378  2llnm3N  34383  lvoli  34389  lvoli3  34391  islvol2aN  34406  4atlem0a  34407  4atlem3  34410  4atlem3a  34411  4atlem4a  34413  4atlem4b  34414  4atlem4c  34415  4atlem4d  34416  4atlem10b  34419  4atlem11  34423  4atlem12  34426  lplncvrlvol2  34429  lvolcmp  34431  2lplnmj  34436  islinei  34554  pmapglbx  34583  linepmap  34589  lneq2at  34592  lnjatN  34594  lncvrat  34596  lncmp  34597  2llnma3r  34602  elpaddatriN  34617  elpaddat  34618  paddcom  34627  paddss1  34631  paddss2  34632  paddss12  34633  paddasslem6  34639  paddasslem7  34640  paddasslem8  34641  paddasslem9  34642  paddasslem15  34648  pmodlem2  34661  pmodl42N  34665  pmapjoin  34666  llnmod1i2  34674  2polcon4bN  34732  polcon2bN  34734  poml4N  34767  poml6N  34769  osumcllem1N  34770  osumcllem2N  34771  osumcllem11N  34780  osumclN  34781  pmapojoinN  34782  pexmidlem2N  34785  pexmidlem3N  34786  pexmidlem4N  34787  pexmidlem6N  34789  pexmidlem7N  34790  pl42lem2N  34794  pl42lem3N  34795  pl42lem4N  34796  pl42N  34797  lhpexle2lem  34823  lhpexle3lem  34825  lhpexle3  34826  lhpmcvr3  34839  lhp2at0nle  34849  lhprelat3N  34854  4atex  34890  4atex2  34891  lauteq  34909  lautco  34911  ltrncoidN  34942  ltrneq2  34962  ltrnnidn  34988  ltrnideq  34989  trlnid  34993  ltrnatlw  34997  trlnle  35000  trlval3  35001  trlval4  35002  cdlemc  35011  cdlemd5  35016  cdlemd9  35020  ltrneq3  35022  cdleme0moN  35039  cdleme20  35138  cdleme21j  35150  cdleme21  35151  cdleme27cl  35180  cdlemefrs29bpre0  35210  cdlemefs27cl  35227  cdlemefs32sn1aw  35228  cdleme43fsv1snlem  35234  cdleme32d  35258  cdleme32f  35260  cdleme32le  35261  cdleme35h2  35271  cdleme38n  35278  cdleme40m  35281  cdleme41snaw  35290  cdleme42ke  35299  cdleme17d3  35310  cdleme48fvg  35314  cdlemeg46fvcl  35320  cdlemeg46fgN  35348  cdleme48gfv1  35350  cdleme48fgv  35352  cdleme50trn3  35367  trlord  35383  ltrniotavalbN  35398  cdlemb3  35420  cdlemg6c  35434  cdlemg6  35437  cdlemg7N  35440  cdlemg8c  35443  cdlemg8  35445  cdlemg11a  35451  cdlemg11b  35456  cdlemg12e  35461  cdlemg15a  35469  cdlemg15  35470  cdlemg16  35471  cdlemg16z  35473  cdlemg16zz  35474  cdlemg17dN  35477  cdlemg18a  35492  cdlemg20  35499  cdlemg22  35501  cdlemg24  35502  cdlemg37  35503  cdlemg31d  35514  cdlemg29  35519  cdlemg33b  35521  cdlemg33  35525  cdlemg38  35529  cdlemg39  35530  cdlemg40  35531  trlco  35541  trlcone  35542  cdlemg42  35543  cdlemg44b  35546  ltrncom  35552  trljco  35554  tendococl  35586  tendoplcl  35595  tendoplcom  35596  cdlemj2  35636  cdlemj3  35637  tendoid0  35639  tendoconid  35643  tendotr  35644  cdlemk25-3  35718  cdlemk26b-3  35719  cdlemk34  35724  cdlemk36  35727  cdlemk38  35729  cdlemkid4  35748  cdlemk35s-id  35752  cdlemk39s-id  35754  cdlemk19x  35757  cdlemk53  35771  cdlemk55  35775  cdlemk55u  35780  cdlemk39u  35782  cdlemk19u  35784  cdlemk56  35785  tendoex  35789  cdleml3N  35792  cdleml5N  35794  tendospcanN  35838  cdlemm10N  35933  cdlemn11pre  36025  dihord2pre  36040  dihvalcqpre  36050  dihopelvalcpre  36063  dihord6apre  36071  dihord5b  36074  dihord5apre  36077  dihord  36079  dihmeetlem1N  36105  dihglblem5apreN  36106  dihglblem3N  36110  dihmeetlem2N  36114  dihglbcpreN  36115  dihmeetbN  36118  dihmeetlem4preN  36121  dihmeetlem5  36123  dihmeetlem7N  36125  dihmeetlem10N  36131  dihmeetlem11N  36132  dihmeetlem12N  36133  dihmeetlem13N  36134  dihmeetlem15N  36136  dihmeetlem16N  36137  dihmeetlem17N  36138  dihmeetlem18N  36139  dihmeetlem19N  36140  dihmeetALTN  36142  dih1dimatlem0  36143  dihlspsnssN  36147  dihlspsnat  36148  mapdh8ad  36594  hdmap14lem14  36699  hgmapvvlem3  36743