Theorem simpl1 1008

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

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  simpll1  1044  simprl1  1050  simp1l1  1098  simp2l1  1104  simp3l1  1110  3anandirs  1367  rspc3ev  3201  brcogw  5023  f1prex  6197  cocan1  6204  weniso  6260  smogt  7094  smorndom  7095  omeulem1  7291  nnmord  7341  nnmword  7342  difsnen  7660  enfixsn  7687  mapunen  7747  ac6sfi  7821  fipreima  7886  elfiun  7950  ordiso2  8030  wemaplem2  8062  wemapso  8066  en2eqpr  8437  indcardi  8470  fodomfi2  8489  iunfictbso  8543  infmap2  8646  cofsmo  8697  cfsmolem  8698  coftr  8701  fin23lem11  8745  fincssdom  8751  fin23lem26  8753  isf32lem9  8789  ac6num  8907  gchdomtri  9053  gchpwdom  9094  winainflem  9117  tskuni  9207  gruima  9226  gruf  9235  grudomon  9241  elnpi  9412  distrlem4pr  9450  prlem934  9457  addcan  9816  addcan2  9817  ltmul1a  10453  ledivmul2OLD  10484  suprleub  10573  supmul1  10576  infmrgelbOLD  10595  suprzcl  11015  uzsupss  11256  xleadd1a  11539  xlesubadd  11549  xmulasslem3  11572  xlemul2a  11575  xadddilem  11580  xadddi2  11583  ixxun  11651  icoshftf1o  11753  snunioc  11758  lincmb01cmp  11773  iccf1o  11774  fzofzim  11960  ltexp2a  12321  leexp2  12324  ltexp2r  12326  exple1  12329  expnlbnd2  12400  ccatass  12719  ccat2s1fvw  12756  swrdswrdlem  12800  ccatopth  12811  cshco  12918  repsco  12921  s2f1o  12980  limsupgre  13520  limsupgreOLD  13521  addcn2  13635  mulcn2  13637  ntrivcvgmul  13936  binomrisefac  14073  dvdsadd2b  14325  dvdsmod  14340  oexpneg  14346  sadass  14419  gcdass  14484  rplpwr  14495  rppwr  14496  lcmass  14544  lcmfunsnlem1  14572  coprmdvds2  14622  rpmulgcd2  14624  qredeq  14625  rpexp  14634  rpdvds  14638  prmdiveq  14694  odzdvds  14700  modprmn0modprm0  14712  coprimeprodsq2  14714  pythagtriplem3  14722  pcdvdsb  14772  pcgcd1  14780  qexpz  14800  pockthg  14804  vdwnnlem1  14899  0ram  14932  ramz2  14936  lubss  16309  lubun  16311  clatleglb  16314  clatglbss  16315  mrelatglb  16372  isnsgrp  16473  issubmnd  16506  ress0g  16507  gsumccat  16567  frmdss2  16589  mulgneg  16718  mulgdirlem  16724  submmulg  16735  subgmulg  16773  nmzsubg  16800  ghmmulg  16837  gsmsymgreqlem1  17013  pmtrfb  17048  psgnunilem4  17080  odmodnn0  17122  odnncl  17127  odmod  17128  odmulgid  17134  odmulgeq  17137  odf1o1  17150  odf1o2  17151  odngen  17155  gexdvdsi  17161  pgpfi1  17173  odcau  17182  subgslw  17194  fislw  17203  lsmssv  17221  lsmless1x  17222  lsmless2x  17223  lsmsubm  17231  lsmmod  17251  lsmmod2  17252  efgred  17324  cntzcmn  17406  ghmplusg  17410  odadd1  17412  odadd2  17413  odadd  17414  lsmcomx  17420  gsumconst  17493  srg1zr  17688  ring1eq0  17746  mulgass2  17755  isabvd  17974  lssintcl  18113  0lmhm  18189  lmhmvsca  18194  reslmhm2b  18203  pwssplit1  18208  pwssplit3  18210  lspfixed  18277  lspsnat  18294  lidldvgen  18405  issubassa  18474  evlsval2  18669  psrplusgpropd  18755  coe1subfv  18785  coe1mul2  18788  xrsdsreclblem  18940  regsumsupp  19112  obselocv  19213  uvcresum  19273  frlmsslsp  19276  frlmup4  19281  lindff1  19300  f1lindf  19302  lsslindf  19310  islindf4  19318  lbslcic  19321  mhmvlin  19344  mpt2matmul  19393  mamutpos  19405  scmatscmide  19454  mavmulsolcl  19498  marrepcl  19511  mdetdiag  19546  mdetunilem1  19559  mdetunilem3  19561  mdetunilem7  19565  mdetunilem9  19567  mdetmul  19570  slesolinvbi  19628  m2pmfzmap  19693  pmatcollpwlem  19726  pmatcollpw  19727  mp2pm2mplem4  19755  chpdmatlem3  19786  chfacfisfcpmat  19801  chfacfscmulgsum  19806  chfacfpmmulgsum  19810  chfacfpmmulgsum2  19811  cayhamlem1  19812  cpmidpmatlem2  19817  cpmadugsumlemB  19820  cpmadugsumlemC  19821  cpmadugsumlemF  19822  riinopn  19860  neiint  20042  topssnei  20062  restntr  20120  iscnp4  20201  cnconst2  20221  cnrest2  20224  cnprest2  20228  cnpdis  20231  cnt0  20284  cnt1  20288  cnhaus  20292  ordthauslem  20321  cncmp  20329  fiuncmp  20341  sscmp  20342  hauscmp  20344  cnconn  20359  uncon  20366  nlly2i  20413  llynlly  20414  nllyidm  20426  finlocfin  20457  ptrescn  20576  xkococnlem  20596  qtoptop2  20636  qtopss  20652  kqfvima  20667  r0cld  20675  ordthmeolem  20738  fbssint  20775  fmf  20882  fmss  20883  elfm  20884  rnelfmlem  20889  rnelfm  20890  fmco  20898  flimss2  20909  flimss1  20910  flimrest  20920  flftg  20933  cnpflf2  20937  cnpflf  20938  flfcnp  20941  supnfcls  20957  fclsss1  20959  fclsss2  20960  fcfnei  20972  fcfelbas  20973  cnpfcfi  20977  subgntr  21043  opnsubg  21044  cldsubg  21047  ghmcnp  21051  utop2nei  21187  neipcfilu  21233  bldisj  21335  blgt0  21336  bl2in  21337  blss2ps  21340  blss2  21341  blssps  21361  blss  21362  xmetresbl  21374  lpbl  21440  blcld  21442  stdbdbl  21454  metcnp3  21477  metcnp2  21479  txmetcnp  21484  blval2  21499  nmoix  21652  nmoeq0  21659  icoopnst  21854  iocopnst  21855  xrhmeo  21861  nmhmcn  22018  cphsqrtcl2  22048  cphsqrtcl3  22049  cfil3i  22123  caublcls  22162  bcthlem5  22180  cmetcusp1  22204  rrxcph  22235  pjth  22265  ovoliunlem2  22325  volun  22366  volsup2  22431  mbfimaopn2  22481  iblconst  22643  itgconst  22644  dvcnp2  22742  dvcn  22743  deg1mul3le  22933  deg1tmle  22934  dvdsq1p  22977  ig1peu  22988  ig1pdvds  22993  coeid3  23053  dgrmulc  23084  efcvx  23260  tanord  23343  logdivlti  23425  logccv  23464  recxpcl  23476  cxpeq  23553  ang180  23599  isosctrlem2  23604  cxp2lim  23758  amgm  23772  muval1  23914  dvdssqf  23919  mumullem2  23961  mumul  23962  bcmono  24059  lgsfcl2  24084  lgsdilem  24104  lgsdirprm  24111  lgsdir  24112  lgsdi  24114  lgsne0  24115  padicabv  24322  brbtwn2  24772  colinearalglem1  24773  colinearalg  24777  axcgrtr  24782  axsegconlem8  24791  axsegconlem9  24792  axsegconlem10  24793  axcontlem8  24838  axcontlem10  24840  2pthon  25168  clwwlkfo  25361  clwwlkext2edg  25366  erclwwlksym  25378  erclwwlknsym  25390  clwlkfoclwwlk  25409  clwlkf1clwwlklem  25413  numclwwlk2lem1  25666  numclwwlk5  25676  frgraregord13  25683  gxcom  25833  gxnn0add  25838  zerdivemp1  25998  nvmul0or  26109  ipval2lem2  26176  ipval2lem5  26182  lnomul  26237  shless  26838  shlej1  26839  pjspansn  27056  hoadddi  27282  kbmul  27434  homco2  27456  kbass2  27596  eliccelico  28186  elicoelioo  28187  iocinioc2  28188  iocinif  28190  xrge0adddir  28284  xrge0npcan  28286  archiabl  28344  ress1r  28382  rhmdvdsr  28411  pstmfval  28529  fmcncfil  28567  zrhnm  28603  qqhnm  28624  measvunilem  28864  volfiniune  28883  dya2iocnrect  28933  sibfinima  28991  probun  29069  probinc  29071  cndprob01  29085  bnj517  29475  bnj594  29502  pconpi1  29739  cvmsss2  29776  mrsubcv  29927  msubvrs  29977  dvdspw  30164  br6  30175  br4  30176  frrlem4  30295  cgrcomim  30532  cgrtriv  30545  cgrextend  30551  segconeq  30553  btwntriv2  30555  btwnintr  30562  btwnexch3  30563  btwnouttr2  30565  trisegint  30571  cgrsub  30588  cgrxfr  30598  btwnxfr  30599  lineext  30619  btwnconn1lem13  30642  btwnconn1lem14  30643  btwnconn3  30646  segcon2  30648  brsegle  30651  brsegle2  30652  segletr  30657  segleantisym  30658  seglelin  30659  outsideofeu  30674  lineunray  30690  lineelsb2  30691  ivthALT  30767  areacirc  31731  cocanfo  31738  upixp  31750  ismtyima  31829  rrndstprj2  31857  zerdivemp1x  31888  lsatfixedN  32274  lssat  32281  eqlkr  32364  eqlkr2  32365  lkrlsp  32367  lshpkrlem4  32378  opposet  32446  cvrcon3b  32542  cvrcmp  32548  atlen0  32575  atnle  32582  atlatmstc  32584  cvlatexch3  32603  cvlsupr2  32608  hlsupr2  32651  hlrelat2  32667  cvrexchlem  32683  lnnat  32691  atcvrj2b  32696  atle  32700  atexchcvrN  32704  atbtwn  32710  athgt  32720  3dimlem3  32725  3dim1  32731  1cvratlt  32738  1cvrjat  32739  ps-1  32741  ps-2  32742  3atlem3  32749  3atlem5  32751  3atlem7  32753  llni  32772  llni2  32776  atcvrlln2  32783  llnexatN  32785  llncmp  32786  2llnmat  32788  2at0mat0  32789  lplni  32796  lplnnle2at  32805  2atnelpln  32808  lplnllnneN  32820  llncvrlpln2  32821  2lplnmN  32823  2llnmj  32824  lplncmp  32826  lplnexatN  32827  lplnexllnN  32828  2llnm3N  32833  lvoli  32839  lvoli3  32841  islvol2aN  32856  4atlem0a  32857  4atlem3  32860  4atlem3a  32861  4atlem4a  32863  4atlem4b  32864  4atlem4c  32865  4atlem4d  32866  4atlem10b  32869  4atlem11  32873  4atlem12  32876  lplncvrlvol2  32879  lvolcmp  32881  2lplnmj  32886  islinei  33004  pmapglbx  33033  linepmap  33039  lneq2at  33042  lnjatN  33044  lncvrat  33046  lncmp  33047  2llnma3r  33052  elpaddatriN  33067  elpaddat  33068  paddcom  33077  paddss1  33081  paddss2  33082  paddss12  33083  paddasslem6  33089  paddasslem7  33090  paddasslem8  33091  paddasslem9  33092  paddasslem15  33098  pmodlem2  33111  pmodl42N  33115  pmapjoin  33116  llnmod1i2  33124  2polcon4bN  33182  polcon2bN  33184  poml4N  33217  poml6N  33219  osumcllem1N  33220  osumcllem2N  33221  osumcllem11N  33230  osumclN  33231  pmapojoinN  33232  pexmidlem2N  33235  pexmidlem3N  33236  pexmidlem4N  33237  pexmidlem6N  33239  pexmidlem7N  33240  pl42lem2N  33244  pl42lem3N  33245  pl42lem4N  33246  pl42N  33247  lhpexle2lem  33273  lhpexle3lem  33275  lhpexle3  33276  lhpmcvr3  33289  lhp2at0nle  33299  lhprelat3N  33304  4atex  33340  4atex2  33341  lauteq  33359  lautco  33361  ltrncoidN  33392  ltrneq2  33412  ltrnnidn  33439  ltrnideq  33440  trlnid  33444  ltrnatlw  33448  trlnle  33451  trlval3  33452  trlval4  33453  cdlemc  33462  cdlemd5  33467  cdlemd9  33471  ltrneq3  33473  cdleme0moN  33490  cdleme20  33590  cdleme21j  33602  cdleme21  33603  cdleme27cl  33632  cdlemefrs29bpre0  33662  cdlemefs27cl  33679  cdlemefs32sn1aw  33680  cdleme43fsv1snlem  33686  cdleme32d  33710  cdleme32f  33712  cdleme32le  33713  cdleme35h2  33723  cdleme38n  33730  cdleme40m  33733  cdleme41snaw  33742  cdleme42ke  33751  cdleme17d3  33762  cdleme48fvg  33766  cdlemeg46fvcl  33772  cdlemeg46fgN  33800  cdleme48gfv1  33802  cdleme48fgv  33804  cdleme50trn3  33819  trlord  33835  ltrniotavalbN  33850  cdlemb3  33872  cdlemg6c  33886  cdlemg6  33889  cdlemg7N  33892  cdlemg8c  33895  cdlemg8  33897  cdlemg11a  33903  cdlemg11b  33908  cdlemg12e  33913  cdlemg15a  33921  cdlemg15  33922  cdlemg16  33923  cdlemg16z  33925  cdlemg16zz  33926  cdlemg17dN  33929  cdlemg18a  33944  cdlemg20  33951  cdlemg22  33953  cdlemg24  33954  cdlemg37  33955  cdlemg31d  33966  cdlemg29  33971  cdlemg33b  33973  cdlemg33  33977  cdlemg38  33981  cdlemg39  33982  cdlemg40  33983  trlco  33993  trlcone  33994  cdlemg42  33995  cdlemg44b  33998  ltrncom  34004  trljco  34006  tendococl  34038  tendoplcl  34047  tendoplcom  34048  cdlemj2  34088  cdlemj3  34089  tendoid0  34091  tendoconid  34095  tendotr  34096  cdlemk25-3  34170  cdlemk26b-3  34171  cdlemk34  34176  cdlemk36  34179  cdlemk38  34181  cdlemkid4  34200  cdlemk35s-id  34204  cdlemk39s-id  34206  cdlemk19x  34209  cdlemk53  34223  cdlemk55  34227  cdlemk55u  34232  cdlemk39u  34234  cdlemk19u  34236  cdlemk56  34237  tendoex  34241  cdleml3N  34244  cdleml5N  34246  tendospcanN  34290  cdlemm10N  34385  cdlemn11pre  34477  dihord2pre  34492  dihvalcqpre  34502  dihopelvalcpre  34515  dihord6apre  34523  dihord5b  34526  dihord5apre  34529  dihord  34531  dihmeetlem1N  34557  dihglblem5apreN  34558  dihglblem3N  34562  dihmeetlem2N  34566  dihglbcpreN  34567  dihmeetbN  34570  dihmeetlem4preN  34573  dihmeetlem5  34575  dihmeetlem7N  34577  dihmeetlem10N  34583  dihmeetlem11N  34584  dihmeetlem12N  34585  dihmeetlem13N  34586  dihmeetlem15N  34588  dihmeetlem16N  34589  dihmeetlem17N  34590  dihmeetlem18N  34591  dihmeetlem19N  34592  dihmeetALTN  34594  dih1dimatlem0  34595  dihlspsnssN  34599  dihlspsnat  34600  mapdh8ad  35046  hdmap14lem14  35151  hgmapvvlem3  35195  mzprename  35290  eldioph2lem1  35301  lzunuz  35309  rencldnfi  35363  pellexlem2  35374  infmrgelbi  35422  pellfundglb  35429  pellfund14gap  35431  qirropth  35452  rmxycomplete  35461  congadd  35512  acongeq  35529  jm2.19  35544  jm2.23  35547  jm2.20nn  35548  jm2.27  35559  jm3.1  35571  aomclem6  35613  lnmepi  35639  lmhmfgsplit  35640  lmhmlnmsplit  35641  pwssplit4  35643  hbtlem2  35679  hbtlem5  35683  dgraa0p  35704  hashgcdlem  35763  proot1hash  35766  iocunico  35784  relexpxpmin  35938  brtrclfv2  35948  suprnmpt  37051  wessf1ornlem  37072  snunioo2  37181  snunioo1  37188  iccintsng  37199  lptre2pt  37282  limcleqr  37287  volioc  37408  iblspltprt  37409  stoweidlem19  37438  stoweidlem20  37439  stoweidlem22  37441  stoweidlem28  37447  stoweidlem34  37454  stoweidlem44  37464  stoweidlem60  37480  wallispilem3  37488  fourierdlem41  37569  fourierdlem42  37570  fourierdlem49  37577  fourierdlem51  37579  fourierdlem54  37582  fourierdlem74  37602  fourierdlem97  37625  caratheodorylem2  37847  fzopredsuc  38100  iccpartigtl  38117  oexpnegALTV  38186  oexpnegnz  38187  tgblthelfgott  38288  repswpfx  38357  fzoopth  38402  lidldomn1  38669  ofaddmndmap  38875  lincdifsn  38967  lincellss  38969  lincresunit3lem3  39017  islindeps2  39026  lindssnlvec  39029  fdivmptf  39103  refdivmptf  39104