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  3133  brcogw  4960  f1prex  6136  cocan1  6143  weniso  6199  smogt  7036  smorndom  7037  omeulem1  7233  nnmord  7283  nnmword  7284  difsnen  7602  enfixsn  7629  mapunen  7689  ac6sfi  7763  fipreima  7828  elfiun  7892  ordiso2  7978  wemaplem2  8010  wemapso  8014  en2eqpr  8385  indcardi  8418  fodomfi2  8437  iunfictbso  8491  infmap2  8594  cofsmo  8645  cfsmolem  8646  coftr  8649  fin23lem11  8693  fincssdom  8699  fin23lem26  8701  isf32lem9  8737  ac6num  8855  gchdomtri  9000  gchpwdom  9041  winainflem  9064  tskuni  9154  gruima  9173  gruf  9182  grudomon  9188  elnpi  9359  distrlem4pr  9397  prlem934  9404  addcan  9763  addcan2  9764  ltmul1a  10400  ledivmul2OLD  10431  suprleub  10519  supmul1  10522  infmrgelbOLD  10541  suprzcl  10961  uzsupss  11202  xleadd1a  11485  xlesubadd  11495  xmulasslem3  11518  xlemul2a  11521  xadddilem  11526  xadddi2  11529  ixxun  11597  icoshftf1o  11701  snunioc  11706  lincmb01cmp  11721  iccf1o  11722  fzofzim  11908  ltexp2a  12269  leexp2  12272  ltexp2r  12274  exple1  12277  expnlbnd2  12348  ccatass  12675  ccat2s1fvw  12712  swrdswrdlem  12756  ccatopth  12767  cshco  12874  repsco  12877  s2f1o  12940  limsupgre  13480  limsupgreOLD  13481  addcn2  13595  mulcn2  13597  ntrivcvgmul  13896  binomrisefac  14033  dvdsadd2b  14285  dvdsmod  14300  oexpneg  14306  sadass  14383  gcdass  14451  rplpwr  14462  rppwr  14463  lcmfunsnlem1  14548  coprmdvds2  14598  rpmulgcd2  14600  qredeq  14601  rpexp  14610  rpdvds  14614  prmdiveq  14672  odzdvds  14678  odzdvdsOLD  14684  modprmn0modprm0  14696  coprimeprodsq2  14698  pythagtriplem3  14706  pcdvdsb  14756  pcgcd1  14764  qexpz  14784  pockthg  14788  vdwnnlem1  14883  0ram  14916  ramz2  14920  lubss  16305  lubun  16307  clatleglb  16310  clatglbss  16311  mrelatglb  16368  isnsgrp  16469  issubmnd  16502  ress0g  16503  gsumccat  16563  frmdss2  16585  mulgneg  16714  mulgdirlem  16720  submmulg  16731  subgmulg  16769  nmzsubg  16796  ghmmulg  16833  gsmsymgreqlem1  17009  pmtrfb  17044  psgnunilem4  17076  odmodnn0  17127  odnncl  17132  odmod  17133  odmulgid  17143  odmulgeq  17146  odf1o1  17159  odf1o2  17160  odngen  17164  gexdvdsi  17172  pgpfi1  17185  odcau  17194  subgslw  17206  fislw  17215  lsmssv  17233  lsmless1x  17234  lsmless2x  17235  lsmsubm  17243  lsmmod  17263  lsmmod2  17264  efgred  17336  cntzcmn  17418  ghmplusg  17422  odadd1  17424  odadd2  17425  odadd  17426  lsmcomx  17432  gsumconst  17505  srg1zr  17700  ring1eq0  17758  mulgass2  17767  isabvd  17986  lssintcl  18125  0lmhm  18201  lmhmvsca  18206  reslmhm2b  18215  pwssplit1  18220  pwssplit3  18222  lspfixed  18289  lspsnat  18306  lidldvgen  18417  issubassa  18486  evlsval2  18681  psrplusgpropd  18767  coe1subfv  18797  coe1mul2  18800  xrsdsreclblem  18952  regsumsupp  19127  obselocv  19228  uvcresum  19288  frlmsslsp  19291  frlmup4  19296  lindff1  19315  f1lindf  19317  lsslindf  19325  islindf4  19333  lbslcic  19336  mhmvlin  19359  mpt2matmul  19408  mamutpos  19420  scmatscmide  19469  mavmulsolcl  19513  marrepcl  19526  mdetdiag  19561  mdetunilem1  19574  mdetunilem3  19576  mdetunilem7  19580  mdetunilem9  19582  mdetmul  19585  slesolinvbi  19643  m2pmfzmap  19708  pmatcollpwlem  19741  pmatcollpw  19742  mp2pm2mplem4  19770  chpdmatlem3  19801  chfacfisfcpmat  19816  chfacfscmulgsum  19821  chfacfpmmulgsum  19825  chfacfpmmulgsum2  19826  cayhamlem1  19827  cpmidpmatlem2  19832  cpmadugsumlemB  19835  cpmadugsumlemC  19836  cpmadugsumlemF  19837  riinopn  19875  neiint  20057  topssnei  20077  restntr  20135  iscnp4  20216  cnconst2  20236  cnrest2  20239  cnprest2  20243  cnpdis  20246  cnt0  20299  cnt1  20303  cnhaus  20307  ordthauslem  20336  cncmp  20344  fiuncmp  20356  sscmp  20357  hauscmp  20359  cnconn  20374  uncon  20381  nlly2i  20428  llynlly  20429  nllyidm  20441  finlocfin  20472  ptrescn  20591  xkococnlem  20611  qtoptop2  20651  qtopss  20667  kqfvima  20682  r0cld  20690  ordthmeolem  20753  fbssint  20790  fmf  20897  fmss  20898  elfm  20899  rnelfmlem  20904  rnelfm  20905  fmco  20913  flimss2  20924  flimss1  20925  flimrest  20935  flftg  20948  cnpflf2  20952  cnpflf  20953  flfcnp  20956  supnfcls  20972  fclsss1  20974  fclsss2  20975  fcfnei  20987  fcfelbas  20988  cnpfcfi  20992  subgntr  21058  opnsubg  21059  cldsubg  21062  ghmcnp  21066  utop2nei  21202  neipcfilu  21248  bldisj  21350  blgt0  21351  bl2in  21352  blss2ps  21355  blss2  21356  blssps  21376  blss  21377  xmetresbl  21389  lpbl  21455  blcld  21457  stdbdbl  21469  metcnp3  21492  metcnp2  21494  txmetcnp  21499  blval2  21514  nmoix  21671  nmoixOLD  21687  nmoeq0  21694  icoopnst  21904  iocopnst  21905  xrhmeo  21911  nmhmcn  22071  cphsqrtcl2  22101  cphsqrtcl3  22102  cfil3i  22176  caublcls  22215  bcthlem5  22233  cmetcusp1  22257  rrxcph  22288  pjth  22330  ovoliunlem2  22393  volun  22435  volsup2  22500  mbfimaopn2  22550  iblconst  22712  itgconst  22713  dvcnp2  22811  dvcn  22812  deg1mul3le  23002  deg1tmle  23003  dvdsq1p  23048  ig1peu  23059  ig1peuOLD  23060  ig1pdvds  23065  ig1pdvdsOLD  23071  coeid3  23131  dgrmulc  23162  efcvx  23341  tanord  23424  logdivlti  23506  logccv  23545  recxpcl  23557  cxpeq  23634  ang180  23680  isosctrlem2  23685  cxp2lim  23839  amgm  23853  muval1  23997  dvdssqf  24002  mumullem2  24044  mumul  24045  bcmono  24142  lgsfcl2  24167  lgsdilem  24187  lgsdirprm  24194  lgsdir  24195  lgsdi  24197  lgsne0  24198  padicabv  24405  brbtwn2  24872  colinearalglem1  24873  colinearalg  24877  axcgrtr  24882  axsegconlem8  24891  axsegconlem9  24892  axsegconlem10  24893  axcontlem8  24938  axcontlem10  24940  2pthon  25269  clwwlkfo  25462  clwwlkext2edg  25467  erclwwlksym  25479  erclwwlknsym  25491  clwlkfoclwwlk  25510  clwlkf1clwwlklem  25514  numclwwlk2lem1  25767  numclwwlk5  25777  frgraregord13  25784  gxcom  25934  gxnn0add  25939  zerdivemp1  26099  nvmul0or  26210  ipval2lem2  26277  ipval2lem5  26283  lnomul  26338  shless  26949  shlej1  26950  pjspansn  27167  hoadddi  27393  kbmul  27545  homco2  27567  kbass2  27707  eliccelico  28304  elicoelioo  28305  iocinioc2  28306  iocinif  28308  xrge0adddir  28401  xrge0npcan  28403  archiabl  28461  ress1r  28499  rhmdvdsr  28528  pstmfval  28646  fmcncfil  28684  zrhnm  28720  qqhnm  28741  measvunilem  28981  volfiniune  29000  dya2iocnrect  29050  sibfinima  29119  probun  29199  probinc  29201  cndprob01  29215  bnj517  29643  bnj594  29670  pconpi1  29907  cvmsss2  29944  mrsubcv  30095  msubvrs  30145  dvdspw  30332  br6  30343  br4  30344  frrlem4  30463  cgrcomim  30700  cgrtriv  30713  cgrextend  30719  segconeq  30721  btwntriv2  30723  btwnintr  30730  btwnexch3  30731  btwnouttr2  30733  trisegint  30739  cgrsub  30756  cgrxfr  30766  btwnxfr  30767  lineext  30787  btwnconn1lem13  30810  btwnconn1lem14  30811  btwnconn3  30814  segcon2  30816  brsegle  30819  brsegle2  30820  segletr  30825  segleantisym  30826  seglelin  30827  outsideofeu  30842  lineunray  30858  lineelsb2  30859  ivthALT  30935  areacirc  31944  cocanfo  31951  upixp  31963  ismtyima  32042  rrndstprj2  32070  zerdivemp1x  32101  lsatfixedN  32487  lssat  32494  eqlkr  32577  eqlkr2  32578  lkrlsp  32580  lshpkrlem4  32591  opposet  32659  cvrcon3b  32755  cvrcmp  32761  atlen0  32788  atnle  32795  atlatmstc  32797  cvlatexch3  32816  cvlsupr2  32821  hlsupr2  32864  hlrelat2  32880  cvrexchlem  32896  lnnat  32904  atcvrj2b  32909  atle  32913  atexchcvrN  32917  atbtwn  32923  athgt  32933  3dimlem3  32938  3dim1  32944  1cvratlt  32951  1cvrjat  32952  ps-1  32954  ps-2  32955  3atlem3  32962  3atlem5  32964  3atlem7  32966  llni  32985  llni2  32989  atcvrlln2  32996  llnexatN  32998  llncmp  32999  2llnmat  33001  2at0mat0  33002  lplni  33009  lplnnle2at  33018  2atnelpln  33021  lplnllnneN  33033  llncvrlpln2  33034  2lplnmN  33036  2llnmj  33037  lplncmp  33039  lplnexatN  33040  lplnexllnN  33041  2llnm3N  33046  lvoli  33052  lvoli3  33054  islvol2aN  33069  4atlem0a  33070  4atlem3  33073  4atlem3a  33074  4atlem4a  33076  4atlem4b  33077  4atlem4c  33078  4atlem4d  33079  4atlem10b  33082  4atlem11  33086  4atlem12  33089  lplncvrlvol2  33092  lvolcmp  33094  2lplnmj  33099  islinei  33217  pmapglbx  33246  linepmap  33252  lneq2at  33255  lnjatN  33257  lncvrat  33259  lncmp  33260  2llnma3r  33265  elpaddatriN  33280  elpaddat  33281  paddcom  33290  paddss1  33294  paddss2  33295  paddss12  33296  paddasslem6  33302  paddasslem7  33303  paddasslem8  33304  paddasslem9  33305  paddasslem15  33311  pmodlem2  33324  pmodl42N  33328  pmapjoin  33329  llnmod1i2  33337  2polcon4bN  33395  polcon2bN  33397  poml4N  33430  poml6N  33432  osumcllem1N  33433  osumcllem2N  33434  osumcllem11N  33443  osumclN  33444  pmapojoinN  33445  pexmidlem2N  33448  pexmidlem3N  33449  pexmidlem4N  33450  pexmidlem6N  33452  pexmidlem7N  33453  pl42lem2N  33457  pl42lem3N  33458  pl42lem4N  33459  pl42N  33460  lhpexle2lem  33486  lhpexle3lem  33488  lhpexle3  33489  lhpmcvr3  33502  lhp2at0nle  33512  lhprelat3N  33517  4atex  33553  4atex2  33554  lauteq  33572  lautco  33574  ltrncoidN  33605  ltrneq2  33625  ltrnnidn  33652  ltrnideq  33653  trlnid  33657  ltrnatlw  33661  trlnle  33664  trlval3  33665  trlval4  33666  cdlemc  33675  cdlemd5  33680  cdlemd9  33684  ltrneq3  33686  cdleme0moN  33703  cdleme20  33803  cdleme21j  33815  cdleme21  33816  cdleme27cl  33845  cdlemefrs29bpre0  33875  cdlemefs27cl  33892  cdlemefs32sn1aw  33893  cdleme43fsv1snlem  33899  cdleme32d  33923  cdleme32f  33925  cdleme32le  33926  cdleme35h2  33936  cdleme38n  33943  cdleme40m  33946  cdleme41snaw  33955  cdleme42ke  33964  cdleme17d3  33975  cdleme48fvg  33979  cdlemeg46fvcl  33985  cdlemeg46fgN  34013  cdleme48gfv1  34015  cdleme48fgv  34017  cdleme50trn3  34032  trlord  34048  ltrniotavalbN  34063  cdlemb3  34085  cdlemg6c  34099  cdlemg6  34102  cdlemg7N  34105  cdlemg8c  34108  cdlemg8  34110  cdlemg11a  34116  cdlemg11b  34121  cdlemg12e  34126  cdlemg15a  34134  cdlemg15  34135  cdlemg16  34136  cdlemg16z  34138  cdlemg16zz  34139  cdlemg17dN  34142  cdlemg18a  34157  cdlemg20  34164  cdlemg22  34166  cdlemg24  34167  cdlemg37  34168  cdlemg31d  34179  cdlemg29  34184  cdlemg33b  34186  cdlemg33  34190  cdlemg38  34194  cdlemg39  34195  cdlemg40  34196  trlco  34206  trlcone  34207  cdlemg42  34208  cdlemg44b  34211  ltrncom  34217  trljco  34219  tendococl  34251  tendoplcl  34260  tendoplcom  34261  cdlemj2  34301  cdlemj3  34302  tendoid0  34304  tendoconid  34308  tendotr  34309  cdlemk25-3  34383  cdlemk26b-3  34384  cdlemk34  34389  cdlemk36  34392  cdlemk38  34394  cdlemkid4  34413  cdlemk35s-id  34417  cdlemk39s-id  34419  cdlemk19x  34422  cdlemk53  34436  cdlemk55  34440  cdlemk55u  34445  cdlemk39u  34447  cdlemk19u  34449  cdlemk56  34450  tendoex  34454  cdleml3N  34457  cdleml5N  34459  tendospcanN  34503  cdlemm10N  34598  cdlemn11pre  34690  dihord2pre  34705  dihvalcqpre  34715  dihopelvalcpre  34728  dihord6apre  34736  dihord5b  34739  dihord5apre  34742  dihord  34744  dihmeetlem1N  34770  dihglblem5apreN  34771  dihglblem3N  34775  dihmeetlem2N  34779  dihglbcpreN  34780  dihmeetbN  34783  dihmeetlem4preN  34786  dihmeetlem5  34788  dihmeetlem7N  34790  dihmeetlem10N  34796  dihmeetlem11N  34797  dihmeetlem12N  34798  dihmeetlem13N  34799  dihmeetlem15N  34801  dihmeetlem16N  34802  dihmeetlem17N  34803  dihmeetlem18N  34804  dihmeetlem19N  34805  dihmeetALTN  34807  dih1dimatlem0  34808  dihlspsnssN  34812  dihlspsnat  34813  mapdh8ad  35259  hdmap14lem14  35364  hgmapvvlem3  35408  mzprename  35503  eldioph2lem1  35514  lzunuz  35522  rencldnfi  35576  pellexlem2  35587  infmrgelbi  35637  infmrgelbiOLD  35638  pellfundglb  35646  pellfund14gap  35648  qirropth  35669  rmxycomplete  35678  congadd  35729  acongeq  35746  jm2.19  35761  jm2.23  35764  jm2.20nn  35765  jm2.27  35776  jm3.1  35788  aomclem6  35830  lnmepi  35856  lmhmfgsplit  35857  lmhmlnmsplit  35858  pwssplit4  35860  hbtlem2  35896  hbtlem5  35900  dgraa0p  35928  hashgcdlem  35987  proot1hash  35990  iocunico  36008  relexpxpmin  36222  brtrclfv2  36232  suprnmpt  37342  wessf1ornlem  37363  projf1o  37378  snunioo2  37498  snunioo1  37505  iccintsng  37516  lptre2pt  37603  limcleqr  37608  volioc  37732  iblspltprt  37733  stoweidlem19  37762  stoweidlem20  37763  stoweidlem22  37765  stoweidlem28  37771  stoweidlem34  37778  stoweidlem44  37788  stoweidlem60  37804  wallispilem3  37812  fourierdlem41  37894  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem49  37902  fourierdlem51  37904  fourierdlem54  37907  fourierdlem74  37927  fourierdlem97  37950  caratheodorylem2  38199  ovnsubaddlem2  38240  fzopredsuc  38533  iccpartigtl  38550  oexpnegALTV  38619  oexpnegnz  38620  tgblthelfgott  38721  repswpfx  38790  fun2dmnop  38833  fzoopth  38860  lidldomn1  39512  ofaddmndmap  39718  lincdifsn  39810  lincellss  39812  lincresunit3lem3  39860  islindeps2  39869  lindssnlvec  39872  fdivmptf  39945  refdivmptf  39946