Theorem simpl1 1000

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 997	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2	1	adantr 465	1 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )

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

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 976

This theorem is referenced by:  simpll1  1036  simprl1  1042  simp1l1  1090  simp2l1  1096  simp3l1  1102  3anandirs  1332  rspc3ev  3209  brcogw  5161  cocan1  6179  weniso  6235  smogt  7040  smorndom  7041  omeulem1  7233  nnmord  7283  nnmword  7284  difsnen  7601  enfixsn  7628  mapunen  7688  ac6sfi  7766  fipreima  7828  elfiun  7892  ordiso2  7943  wemaplem2  7975  wemapso  7979  en2eqpr  8388  indcardi  8425  fodomfi2  8444  iunfictbso  8498  infmap2  8601  cofsmo  8652  cfsmolem  8653  coftr  8656  fin23lem11  8700  fincssdom  8706  fin23lem26  8708  isf32lem9  8744  ac6num  8862  gchdomtri  9010  gchpwdom  9051  winainflem  9074  tskuni  9164  gruima  9183  gruf  9192  grudomon  9198  elnpi  9369  distrlem4pr  9407  prlem934  9414  addcan  9767  addcan2  9768  ltmul1a  10397  ledivmulOLD  10425  ledivmul2OLD  10429  suprleub  10513  supmul1  10514  infmrgelb  10529  suprzcl  10948  uzsupss  11183  xleadd1a  11454  xlesubadd  11464  xmulasslem3  11487  xlemul2a  11490  xadddilem  11495  xadddi2  11498  ixxun  11554  icoshftf1o  11652  snunioc  11657  lincmb01cmp  11672  iccf1o  11673  fzofzim  11848  ltexp2a  12196  leexp2  12199  ltexp2r  12201  exple1  12204  expnlbnd2  12276  ccatass  12584  swrdswrdlem  12663  ccatopth  12674  cshco  12781  repsco  12784  s2f1o  12843  limsupgre  13283  addcn2  13395  mulcn2  13397  dvdsadd2b  13905  dvdsmod  13920  oexpneg  13926  sadass  13998  gcdass  14060  rplpwr  14071  rppwr  14072  coprmdvds2  14121  rpmulgcd2  14123  qredeq  14124  rpexp  14138  rpdvds  14142  prmdiveq  14193  odzdvds  14199  modprmn0modprm0  14209  coprimeprodsq2  14211  pythagtriplem3  14219  pcdvdsb  14269  pcgcd1  14277  qexpz  14297  pockthg  14301  vdwnnlem1  14390  0ram  14415  ramz2  14419  lubss  15625  lubun  15627  clatleglb  15630  clatglbss  15631  mrelatglb  15688  isnsgrp  15789  issubmnd  15822  ress0g  15823  gsumccat  15883  frmdss2  15905  mulgneg  16034  mulgdirlem  16040  submmulg  16051  subgmulg  16089  nmzsubg  16116  ghmmulg  16153  gsmsymgreqlem1  16329  pmtrfb  16364  psgnunilem4  16396  odmodnn0  16438  odnncl  16443  odmod  16444  odmulgid  16450  odmulgeq  16453  odf1o1  16466  odf1o2  16467  odngen  16471  gexdvdsi  16477  pgpfi1  16489  odcau  16498  subgslw  16510  fislw  16519  lsmssv  16537  lsmless1x  16538  lsmless2x  16539  lsmsubm  16547  lsmmod  16567  lsmmod2  16568  efgred  16640  cntzcmn  16722  ghmplusg  16726  odadd1  16728  odadd2  16729  odadd  16730  lsmcomx  16736  gsumconst  16828  srg1zr  17054  ring1eq0  17112  mulgass2  17121  isabvd  17343  lssintcl  17484  0lmhm  17560  lmhmvsca  17565  reslmhm2b  17574  pwssplit1  17579  pwssplit3  17581  lspfixed  17648  lspsnat  17665  lidldvgen  17777  issubassa  17847  evlsval2  18063  psrplusgpropd  18151  coe1subfv  18181  coe1mul2  18184  xrsdsreclblem  18338  regsumsupp  18531  obselocv  18632  uvcresum  18697  frlmsslsp  18702  frlmsslspOLD  18703  frlmup4  18708  lindff1  18728  f1lindf  18730  lsslindf  18738  islindf4  18746  lbslcic  18749  mhmvlin  18772  mpt2matmul  18821  mamutpos  18833  scmatscmide  18882  mavmulsolcl  18926  marrepcl  18939  mdetdiag  18974  mdetunilem1  18987  mdetunilem3  18989  mdetunilem7  18993  mdetunilem9  18995  mdetmul  18998  slesolinvbi  19056  m2pmfzmap  19121  pmatcollpwlem  19154  pmatcollpw  19155  mp2pm2mplem4  19183  chpdmatlem3  19214  chfacfisfcpmat  19229  chfacfscmulgsum  19234  chfacfpmmulgsum  19238  chfacfpmmulgsum2  19239  cayhamlem1  19240  cpmidpmatlem2  19245  cpmadugsumlemB  19248  cpmadugsumlemC  19249  cpmadugsumlemF  19250  riinopn  19290  neiint  19478  topssnei  19498  restntr  19556  iscnp4  19637  cnconst2  19657  cnrest2  19660  cnprest2  19664  cnpdis  19667  cnt0  19720  cnt1  19724  cnhaus  19728  ordthauslem  19757  cncmp  19765  fiuncmp  19777  sscmp  19778  hauscmp  19780  cnconn  19796  uncon  19803  nlly2i  19850  llynlly  19851  nllyidm  19863  finlocfin  19894  ptrescn  20013  xkococnlem  20033  qtoptop2  20073  qtopss  20089  kqfvima  20104  r0cld  20112  ordthmeolem  20175  fbssint  20212  fmf  20319  fmss  20320  elfm  20321  rnelfmlem  20326  rnelfm  20327  fmco  20335  flimss2  20346  flimss1  20347  flimrest  20357  flftg  20370  cnpflf2  20374  cnpflf  20375  flfcnp  20378  supnfcls  20394  fclsss1  20396  fclsss2  20397  fcfnei  20409  fcfelbas  20410  cnpfcfi  20414  subgntr  20478  opnsubg  20479  cldsubg  20482  ghmcnp  20486  utop2nei  20626  neipcfilu  20672  bldisj  20774  blgt0  20775  bl2in  20776  blss2ps  20779  blss2  20780  blssps  20800  blss  20801  xmetresbl  20813  lpbl  20879  blcld  20881  stdbdbl  20893  metcnp3  20916  metcnp2  20918  txmetcnp  20923  blval2  20951  nmoix  21109  nmoeq0  21116  icoopnst  21312  iocopnst  21313  xrhmeo  21319  nmhmcn  21476  cphsqrtcl2  21506  cphsqrtcl3  21507  cfil3i  21581  caublcls  21620  bcthlem5  21640  cmetcusp1OLD  21664  cmetcusp1  21665  rrxcph  21697  pjth  21727  ovoliunlem2  21787  volun  21828  volsup2  21887  mbfimaopn2  21937  iblconst  22097  itgconst  22098  dvcnp2  22196  dvcn  22197  deg1mul3le  22390  deg1tmle  22391  dvdsq1p  22434  ig1peu  22445  ig1pdvds  22450  coeid3  22510  dgrmulc  22540  efcvx  22716  tanord  22797  logdivlti  22877  logccv  22916  recxpcl  22928  cxpeq  23003  ang180  23018  isosctrlem2  23025  cxp2lim  23178  amgm  23192  muval1  23279  dvdssqf  23284  mumullem2  23326  mumul  23327  bcmono  23424  lgsfcl2  23449  lgsdilem  23469  lgsdirprm  23476  lgsdir  23477  lgsdi  23479  lgsne0  23480  padicabv  23687  brbtwn2  24080  colinearalglem1  24081  colinearalg  24085  axcgrtr  24090  axsegconlem8  24099  axsegconlem9  24100  axsegconlem10  24101  axcontlem8  24146  axcontlem10  24148  2pthon  24476  clwwlkfo  24669  clwwlkext2edg  24674  erclwwlksym  24686  erclwwlknsym  24698  clwlkfoclwwlk  24717  clwlkf1clwwlklem  24721  numclwwlk2lem1  24974  numclwwlk5  24984  frgraregord13  24991  gxcom  25143  gxnn0add  25148  zerdivemp1  25308  nvmul0or  25419  ipval2lem2  25486  ipval2lem5  25492  lnomul  25547  shless  26149  shlej1  26150  pjspansn  26367  hoadddi  26594  kbmul  26746  homco2  26768  kbass2  26908  eliccelico  27460  elicoelioo  27461  iocinioc2  27462  iocinif  27464  xrge0adddir  27555  xrge0npcan  27557  archiabl  27615  ress1r  27652  rhmdvdsr  27681  pstmfval  27748  fmcncfil  27786  zrhnm  27823  qqhnm  27844  measvunilem  28056  volfiniune  28075  dya2iocnrect  28125  sibfinima  28154  probun  28231  probinc  28233  cndprob01  28247  pconpi1  28555  cvmsss2  28592  mrsubcv  28743  msubvrs  28793  ntrivcvgmul  29011  binomrisefac  29139  dvdspw  29150  br6  29161  br4  29162  frrlem4  29365  cgrcomim  29614  cgrtriv  29627  cgrextend  29633  segconeq  29635  btwntriv2  29637  btwnintr  29644  btwnexch3  29645  btwnouttr2  29647  trisegint  29653  cgrsub  29670  cgrxfr  29680  btwnxfr  29681  lineext  29701  btwnconn1lem13  29724  btwnconn1lem14  29725  btwnconn3  29728  segcon2  29730  brsegle  29733  brsegle2  29734  segletr  29739  segleantisym  29740  seglelin  29741  outsideofeu  29756  lineunray  29772  lineelsb2  29773  areacirc  30087  ivthALT  30128  cocanfo  30183  upixp  30195  ismtyima  30274  rrndstprj2  30302  zerdivemp1x  30333  mzprename  30657  eldioph2lem1  30668  lzunuz  30676  rencldnfi  30730  pellexlem2  30741  infmrgelbi  30789  pellfundglb  30796  pellfund14gap  30798  qirropth  30819  rmxycomplete  30828  congadd  30879  acongeq  30896  jm2.19  30910  jm2.23  30913  jm2.20nn  30914  jm2.27  30925  jm3.1  30937  aomclem6  30980  lnmepi  31006  lmhmfgsplit  31007  lmhmlnmsplit  31008  pwssplit4  31010  hbtlem2  31048  hbtlem5  31052  dgraa0p  31074  hashgcdlem  31133  proot1hash  31136  iocunico  31154  lcmass  31194  suprnmpt  31401  snunioo2  31480  snunioo1  31488  iccintsng  31499  lptre2pt  31554  limcleqr  31558  volioc  31661  iblspltprt  31662  stoweidlem19  31690  stoweidlem20  31691  stoweidlem22  31693  stoweidlem28  31699  stoweidlem34  31705  stoweidlem44  31715  stoweidlem60  31731  wallispilem3  31738  fourierdlem41  31819  fourierdlem42  31820  fourierdlem49  31827  fourierdlem51  31829  fourierdlem54  31832  fourierdlem74  31852  fourierdlem97  31875  fzoopth  32178  lidldomn1  32437  ofaddmndmap  32666  lincdifsn  32760  lincellss  32762  lincresunit3lem3  32810  islindeps2  32819  lindssnlvec  32822  bnj517  33676  bnj594  33703  lsatfixedN  34474  lssat  34481  eqlkr  34564  eqlkr2  34565  lkrlsp  34567  lshpkrlem4  34578  opposet  34646  cvrcon3b  34742  cvrcmp  34748  atlen0  34775  atnle  34782  atlatmstc  34784  cvlatexch3  34803  cvlsupr2  34808  hlsupr2  34851  hlrelat2  34867  cvrexchlem  34883  lnnat  34891  atcvrj2b  34896  atle  34900  atexchcvrN  34904  atbtwn  34910  athgt  34920  3dimlem3  34925  3dim1  34931  1cvratlt  34938  1cvrjat  34939  ps-1  34941  ps-2  34942  3atlem3  34949  3atlem5  34951  3atlem7  34953  llni  34972  llni2  34976  atcvrlln2  34983  llnexatN  34985  llncmp  34986  2llnmat  34988  2at0mat0  34989  lplni  34996  lplnnle2at  35005  2atnelpln  35008  lplnllnneN  35020  llncvrlpln2  35021  2lplnmN  35023  2llnmj  35024  lplncmp  35026  lplnexatN  35027  lplnexllnN  35028  2llnm3N  35033  lvoli  35039  lvoli3  35041  islvol2aN  35056  4atlem0a  35057  4atlem3  35060  4atlem3a  35061  4atlem4a  35063  4atlem4b  35064  4atlem4c  35065  4atlem4d  35066  4atlem10b  35069  4atlem11  35073  4atlem12  35076  lplncvrlvol2  35079  lvolcmp  35081  2lplnmj  35086  islinei  35204  pmapglbx  35233  linepmap  35239  lneq2at  35242  lnjatN  35244  lncvrat  35246  lncmp  35247  2llnma3r  35252  elpaddatriN  35267  elpaddat  35268  paddcom  35277  paddss1  35281  paddss2  35282  paddss12  35283  paddasslem6  35289  paddasslem7  35290  paddasslem8  35291  paddasslem9  35292  paddasslem15  35298  pmodlem2  35311  pmodl42N  35315  pmapjoin  35316  llnmod1i2  35324  2polcon4bN  35382  polcon2bN  35384  poml4N  35417  poml6N  35419  osumcllem1N  35420  osumcllem2N  35421  osumcllem11N  35430  osumclN  35431  pmapojoinN  35432  pexmidlem2N  35435  pexmidlem3N  35436  pexmidlem4N  35437  pexmidlem6N  35439  pexmidlem7N  35440  pl42lem2N  35444  pl42lem3N  35445  pl42lem4N  35446  pl42N  35447  lhpexle2lem  35473  lhpexle3lem  35475  lhpexle3  35476  lhpmcvr3  35489  lhp2at0nle  35499  lhprelat3N  35504  4atex  35540  4atex2  35541  lauteq  35559  lautco  35561  ltrncoidN  35592  ltrneq2  35612  ltrnnidn  35639  ltrnideq  35640  trlnid  35644  ltrnatlw  35648  trlnle  35651  trlval3  35652  trlval4  35653  cdlemc  35662  cdlemd5  35667  cdlemd9  35671  ltrneq3  35673  cdleme0moN  35690  cdleme20  35790  cdleme21j  35802  cdleme21  35803  cdleme27cl  35832  cdlemefrs29bpre0  35862  cdlemefs27cl  35879  cdlemefs32sn1aw  35880  cdleme43fsv1snlem  35886  cdleme32d  35910  cdleme32f  35912  cdleme32le  35913  cdleme35h2  35923  cdleme38n  35930  cdleme40m  35933  cdleme41snaw  35942  cdleme42ke  35951  cdleme17d3  35962  cdleme48fvg  35966  cdlemeg46fvcl  35972  cdlemeg46fgN  36000  cdleme48gfv1  36002  cdleme48fgv  36004  cdleme50trn3  36019  trlord  36035  ltrniotavalbN  36050  cdlemb3  36072  cdlemg6c  36086  cdlemg6  36089  cdlemg7N  36092  cdlemg8c  36095  cdlemg8  36097  cdlemg11a  36103  cdlemg11b  36108  cdlemg12e  36113  cdlemg15a  36121  cdlemg15  36122  cdlemg16  36123  cdlemg16z  36125  cdlemg16zz  36126  cdlemg17dN  36129  cdlemg18a  36144  cdlemg20  36151  cdlemg22  36153  cdlemg24  36154  cdlemg37  36155  cdlemg31d  36166  cdlemg29  36171  cdlemg33b  36173  cdlemg33  36177  cdlemg38  36181  cdlemg39  36182  cdlemg40  36183  trlco  36193  trlcone  36194  cdlemg42  36195  cdlemg44b  36198  ltrncom  36204  trljco  36206  tendococl  36238  tendoplcl  36247  tendoplcom  36248  cdlemj2  36288  cdlemj3  36289  tendoid0  36291  tendoconid  36295  tendotr  36296  cdlemk25-3  36370  cdlemk26b-3  36371  cdlemk34  36376  cdlemk36  36379  cdlemk38  36381  cdlemkid4  36400  cdlemk35s-id  36404  cdlemk39s-id  36406  cdlemk19x  36409  cdlemk53  36423  cdlemk55  36427  cdlemk55u  36432  cdlemk39u  36434  cdlemk19u  36436  cdlemk56  36437  tendoex  36441  cdleml3N  36444  cdleml5N  36446  tendospcanN  36490  cdlemm10N  36585  cdlemn11pre  36677  dihord2pre  36692  dihvalcqpre  36702  dihopelvalcpre  36715  dihord6apre  36723  dihord5b  36726  dihord5apre  36729  dihord  36731  dihmeetlem1N  36757  dihglblem5apreN  36758  dihglblem3N  36762  dihmeetlem2N  36766  dihglbcpreN  36767  dihmeetbN  36770  dihmeetlem4preN  36773  dihmeetlem5  36775  dihmeetlem7N  36777  dihmeetlem10N  36783  dihmeetlem11N  36784  dihmeetlem12N  36785  dihmeetlem13N  36786  dihmeetlem15N  36788  dihmeetlem16N  36789  dihmeetlem17N  36790  dihmeetlem18N  36791  dihmeetlem19N  36792  dihmeetALTN  36794  dih1dimatlem0  36795  dihlspsnssN  36799  dihlspsnat  36800  mapdh8ad  37246  hdmap14lem14  37351  hgmapvvlem3  37395