Theorem simpl1 1017

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

Syntax hints:   -> wi 4   /\ wa 375   /\ w3a 991

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 190  df-an 377  df-3an 993

This theorem is referenced by:  simpll1  1053  simprl1  1059  simp1l1  1107  simp2l1  1113  simp3l1  1119  3anandirs  1382  rspc3ev  3175  brcogw  5022  f1prex  6207  cocan1  6214  weniso  6270  smogt  7112  smorndom  7113  omeulem1  7309  nnmord  7359  nnmword  7360  difsnen  7680  enfixsn  7707  mapunen  7767  ac6sfi  7841  fipreima  7906  elfiun  7970  ordiso2  8056  wemaplem2  8088  wemapso  8092  en2eqpr  8464  indcardi  8498  fodomfi2  8517  iunfictbso  8571  infmap2  8674  cofsmo  8725  cfsmolem  8726  coftr  8729  fin23lem11  8773  fincssdom  8779  fin23lem26  8781  isf32lem9  8817  ac6num  8935  gchdomtri  9080  gchpwdom  9121  winainflem  9144  tskuni  9234  gruima  9253  gruf  9262  grudomon  9268  elnpi  9439  distrlem4pr  9477  prlem934  9484  addcan  9843  addcan2  9844  ltmul1a  10482  ledivmul2OLD  10513  suprleub  10601  supmul1  10604  infmrgelbOLD  10623  suprzcl  11044  uzsupss  11285  xleadd1a  11568  xlesubadd  11578  xmulasslem3  11601  xlemul2a  11604  xadddilem  11609  xadddi2  11612  ixxun  11680  icoshftf1o  11784  snunioc  11789  lincmb01cmp  11804  iccf1o  11805  fzofzim  11993  ltexp2a  12356  leexp2  12359  ltexp2r  12361  exple1  12364  expnlbnd2  12435  ccatass  12768  ccat2s1fvw  12808  swrdswrdlem  12852  ccatopth  12863  cshco  12970  repsco  12973  s2f1o  13047  limsupgre  13591  limsupgreOLD  13592  addcn2  13706  mulcn2  13708  ntrivcvgmul  14007  binomrisefac  14144  dvdsadd2b  14396  dvdsmod  14411  oexpneg  14417  sadass  14494  gcdass  14562  rplpwr  14573  rppwr  14574  lcmfunsnlem1  14659  coprmdvds2  14709  rpmulgcd2  14711  qredeq  14712  rpexp  14721  rpdvds  14725  prmdiveq  14783  odzdvds  14789  odzdvdsOLD  14795  modprmn0modprm0  14807  coprimeprodsq2  14809  pythagtriplem3  14817  pcdvdsb  14867  pcgcd1  14875  qexpz  14895  pockthg  14899  vdwnnlem1  14994  0ram  15027  ramz2  15031  lubss  16416  lubun  16418  clatleglb  16421  clatglbss  16422  mrelatglb  16479  isnsgrp  16580  issubmnd  16613  ress0g  16614  gsumccat  16674  frmdss2  16696  mulgneg  16825  mulgdirlem  16831  submmulg  16842  subgmulg  16880  nmzsubg  16907  ghmmulg  16944  gsmsymgreqlem1  17120  pmtrfb  17155  psgnunilem4  17187  odmodnn0  17238  odnncl  17243  odmod  17244  odmulgid  17254  odmulgeq  17257  odf1o1  17270  odf1o2  17271  odngen  17275  gexdvdsi  17283  pgpfi1  17296  odcau  17305  subgslw  17317  fislw  17326  lsmssv  17344  lsmless1x  17345  lsmless2x  17346  lsmsubm  17354  lsmmod  17374  lsmmod2  17375  efgred  17447  cntzcmn  17529  ghmplusg  17533  odadd1  17535  odadd2  17536  odadd  17537  lsmcomx  17543  gsumconst  17616  srg1zr  17811  ring1eq0  17869  mulgass2  17878  isabvd  18097  lssintcl  18236  0lmhm  18312  lmhmvsca  18317  reslmhm2b  18326  pwssplit1  18331  pwssplit3  18333  lspfixed  18400  lspsnat  18417  lidldvgen  18528  issubassa  18597  evlsval2  18792  psrplusgpropd  18878  coe1subfv  18908  coe1mul2  18911  xrsdsreclblem  19063  regsumsupp  19239  obselocv  19340  uvcresum  19400  frlmsslsp  19403  frlmup4  19408  lindff1  19427  f1lindf  19429  lsslindf  19437  islindf4  19445  lbslcic  19448  mhmvlin  19471  mpt2matmul  19520  mamutpos  19532  scmatscmide  19581  mavmulsolcl  19625  marrepcl  19638  mdetdiag  19673  mdetunilem1  19686  mdetunilem3  19688  mdetunilem7  19692  mdetunilem9  19694  mdetmul  19697  slesolinvbi  19755  m2pmfzmap  19820  pmatcollpwlem  19853  pmatcollpw  19854  mp2pm2mplem4  19882  chpdmatlem3  19913  chfacfisfcpmat  19928  chfacfscmulgsum  19933  chfacfpmmulgsum  19937  chfacfpmmulgsum2  19938  cayhamlem1  19939  cpmidpmatlem2  19944  cpmadugsumlemB  19947  cpmadugsumlemC  19948  cpmadugsumlemF  19949  riinopn  19987  neiint  20169  topssnei  20189  restntr  20247  iscnp4  20328  cnconst2  20348  cnrest2  20351  cnprest2  20355  cnpdis  20358  cnt0  20411  cnt1  20415  cnhaus  20419  ordthauslem  20448  cncmp  20456  fiuncmp  20468  sscmp  20469  hauscmp  20471  cnconn  20486  uncon  20493  nlly2i  20540  llynlly  20541  nllyidm  20553  finlocfin  20584  ptrescn  20703  xkococnlem  20723  qtoptop2  20763  qtopss  20779  kqfvima  20794  r0cld  20802  ordthmeolem  20865  fbssint  20902  fmf  21009  fmss  21010  elfm  21011  rnelfmlem  21016  rnelfm  21017  fmco  21025  flimss2  21036  flimss1  21037  flimrest  21047  flftg  21060  cnpflf2  21064  cnpflf  21065  flfcnp  21068  supnfcls  21084  fclsss1  21086  fclsss2  21087  fcfnei  21099  fcfelbas  21100  cnpfcfi  21104  subgntr  21170  opnsubg  21171  cldsubg  21174  ghmcnp  21178  utop2nei  21314  neipcfilu  21360  bldisj  21462  blgt0  21463  bl2in  21464  blss2ps  21467  blss2  21468  blssps  21488  blss  21489  xmetresbl  21501  lpbl  21567  blcld  21569  stdbdbl  21581  metcnp3  21604  metcnp2  21606  txmetcnp  21611  blval2  21626  nmoix  21783  nmoixOLD  21799  nmoeq0  21806  icoopnst  22016  iocopnst  22017  xrhmeo  22023  nmhmcn  22183  cphsqrtcl2  22213  cphsqrtcl3  22214  cfil3i  22288  caublcls  22327  bcthlem5  22345  cmetcusp1  22369  rrxcph  22400  pjth  22442  ovoliunlem2  22505  volun  22547  volsup2  22612  mbfimaopn2  22662  iblconst  22824  itgconst  22825  dvcnp2  22923  dvcn  22924  deg1mul3le  23114  deg1tmle  23115  dvdsq1p  23160  ig1peu  23171  ig1peuOLD  23172  ig1pdvds  23177  ig1pdvdsOLD  23183  coeid3  23243  dgrmulc  23274  efcvx  23453  tanord  23536  logdivlti  23618  logccv  23657  recxpcl  23669  cxpeq  23746  ang180  23792  isosctrlem2  23797  cxp2lim  23951  amgm  23965  muval1  24109  dvdssqf  24114  mumullem2  24156  mumul  24157  bcmono  24254  lgsfcl2  24279  lgsdilem  24299  lgsdirprm  24306  lgsdir  24307  lgsdi  24309  lgsne0  24310  padicabv  24517  brbtwn2  24984  colinearalglem1  24985  colinearalg  24989  axcgrtr  24994  axsegconlem8  25003  axsegconlem9  25004  axsegconlem10  25005  axcontlem8  25050  axcontlem10  25052  2pthon  25381  clwwlkfo  25574  clwwlkext2edg  25579  erclwwlksym  25591  erclwwlknsym  25603  clwlkfoclwwlk  25622  clwlkf1clwwlklem  25626  numclwwlk2lem1  25879  numclwwlk5  25889  frgraregord13  25896  gxcom  26046  gxnn0add  26051  zerdivemp1  26211  nvmul0or  26322  ipval2lem2  26389  ipval2lem5  26395  lnomul  26450  shless  27061  shlej1  27062  pjspansn  27279  hoadddi  27505  kbmul  27657  homco2  27679  kbass2  27819  eliccelico  28408  elicoelioo  28409  iocinioc2  28410  iocinif  28412  xrge0adddir  28504  xrge0npcan  28506  archiabl  28564  ress1r  28601  rhmdvdsr  28630  pstmfval  28748  fmcncfil  28786  zrhnm  28822  qqhnm  28843  measvunilem  29083  volfiniune  29102  dya2iocnrect  29152  sibfinima  29221  probun  29301  probinc  29303  cndprob01  29317  bnj517  29745  bnj594  29772  pconpi1  30009  cvmsss2  30046  mrsubcv  30197  msubvrs  30247  dvdspw  30435  br6  30446  br4  30447  frrlem4  30566  cgrcomim  30805  cgrtriv  30818  cgrextend  30824  segconeq  30826  btwntriv2  30828  btwnintr  30835  btwnexch3  30836  btwnouttr2  30838  trisegint  30844  cgrsub  30861  cgrxfr  30871  btwnxfr  30872  lineext  30892  btwnconn1lem13  30915  btwnconn1lem14  30916  btwnconn3  30919  segcon2  30921  brsegle  30924  brsegle2  30925  segletr  30930  segleantisym  30931  seglelin  30932  outsideofeu  30947  lineunray  30963  lineelsb2  30964  ivthALT  31040  areacirc  32082  cocanfo  32089  upixp  32101  ismtyima  32180  rrndstprj2  32208  zerdivemp1x  32239  lsatfixedN  32620  lssat  32627  eqlkr  32710  eqlkr2  32711  lkrlsp  32713  lshpkrlem4  32724  opposet  32792  cvrcon3b  32888  cvrcmp  32894  atlen0  32921  atnle  32928  atlatmstc  32930  cvlatexch3  32949  cvlsupr2  32954  hlsupr2  32997  hlrelat2  33013  cvrexchlem  33029  lnnat  33037  atcvrj2b  33042  atle  33046  atexchcvrN  33050  atbtwn  33056  athgt  33066  3dimlem3  33071  3dim1  33077  1cvratlt  33084  1cvrjat  33085  ps-1  33087  ps-2  33088  3atlem3  33095  3atlem5  33097  3atlem7  33099  llni  33118  llni2  33122  atcvrlln2  33129  llnexatN  33131  llncmp  33132  2llnmat  33134  2at0mat0  33135  lplni  33142  lplnnle2at  33151  2atnelpln  33154  lplnllnneN  33166  llncvrlpln2  33167  2lplnmN  33169  2llnmj  33170  lplncmp  33172  lplnexatN  33173  lplnexllnN  33174  2llnm3N  33179  lvoli  33185  lvoli3  33187  islvol2aN  33202  4atlem0a  33203  4atlem3  33206  4atlem3a  33207  4atlem4a  33209  4atlem4b  33210  4atlem4c  33211  4atlem4d  33212  4atlem10b  33215  4atlem11  33219  4atlem12  33222  lplncvrlvol2  33225  lvolcmp  33227  2lplnmj  33232  islinei  33350  pmapglbx  33379  linepmap  33385  lneq2at  33388  lnjatN  33390  lncvrat  33392  lncmp  33393  2llnma3r  33398  elpaddatriN  33413  elpaddat  33414  paddcom  33423  paddss1  33427  paddss2  33428  paddss12  33429  paddasslem6  33435  paddasslem7  33436  paddasslem8  33437  paddasslem9  33438  paddasslem15  33444  pmodlem2  33457  pmodl42N  33461  pmapjoin  33462  llnmod1i2  33470  2polcon4bN  33528  polcon2bN  33530  poml4N  33563  poml6N  33565  osumcllem1N  33566  osumcllem2N  33567  osumcllem11N  33576  osumclN  33577  pmapojoinN  33578  pexmidlem2N  33581  pexmidlem3N  33582  pexmidlem4N  33583  pexmidlem6N  33585  pexmidlem7N  33586  pl42lem2N  33590  pl42lem3N  33591  pl42lem4N  33592  pl42N  33593  lhpexle2lem  33619  lhpexle3lem  33621  lhpexle3  33622  lhpmcvr3  33635  lhp2at0nle  33645  lhprelat3N  33650  4atex  33686  4atex2  33687  lauteq  33705  lautco  33707  ltrncoidN  33738  ltrneq2  33758  ltrnnidn  33785  ltrnideq  33786  trlnid  33790  ltrnatlw  33794  trlnle  33797  trlval3  33798  trlval4  33799  cdlemc  33808  cdlemd5  33813  cdlemd9  33817  ltrneq3  33819  cdleme0moN  33836  cdleme20  33936  cdleme21j  33948  cdleme21  33949  cdleme27cl  33978  cdlemefrs29bpre0  34008  cdlemefs27cl  34025  cdlemefs32sn1aw  34026  cdleme43fsv1snlem  34032  cdleme32d  34056  cdleme32f  34058  cdleme32le  34059  cdleme35h2  34069  cdleme38n  34076  cdleme40m  34079  cdleme41snaw  34088  cdleme42ke  34097  cdleme17d3  34108  cdleme48fvg  34112  cdlemeg46fvcl  34118  cdlemeg46fgN  34146  cdleme48gfv1  34148  cdleme48fgv  34150  cdleme50trn3  34165  trlord  34181  ltrniotavalbN  34196  cdlemb3  34218  cdlemg6c  34232  cdlemg6  34235  cdlemg7N  34238  cdlemg8c  34241  cdlemg8  34243  cdlemg11a  34249  cdlemg11b  34254  cdlemg12e  34259  cdlemg15a  34267  cdlemg15  34268  cdlemg16  34269  cdlemg16z  34271  cdlemg16zz  34272  cdlemg17dN  34275  cdlemg18a  34290  cdlemg20  34297  cdlemg22  34299  cdlemg24  34300  cdlemg37  34301  cdlemg31d  34312  cdlemg29  34317  cdlemg33b  34319  cdlemg33  34323  cdlemg38  34327  cdlemg39  34328  cdlemg40  34329  trlco  34339  trlcone  34340  cdlemg42  34341  cdlemg44b  34344  ltrncom  34350  trljco  34352  tendococl  34384  tendoplcl  34393  tendoplcom  34394  cdlemj2  34434  cdlemj3  34435  tendoid0  34437  tendoconid  34441  tendotr  34442  cdlemk25-3  34516  cdlemk26b-3  34517  cdlemk34  34522  cdlemk36  34525  cdlemk38  34527  cdlemkid4  34546  cdlemk35s-id  34550  cdlemk39s-id  34552  cdlemk19x  34555  cdlemk53  34569  cdlemk55  34573  cdlemk55u  34578  cdlemk39u  34580  cdlemk19u  34582  cdlemk56  34583  tendoex  34587  cdleml3N  34590  cdleml5N  34592  tendospcanN  34636  cdlemm10N  34731  cdlemn11pre  34823  dihord2pre  34838  dihvalcqpre  34848  dihopelvalcpre  34861  dihord6apre  34869  dihord5b  34872  dihord5apre  34875  dihord  34877  dihmeetlem1N  34903  dihglblem5apreN  34904  dihglblem3N  34908  dihmeetlem2N  34912  dihglbcpreN  34913  dihmeetbN  34916  dihmeetlem4preN  34919  dihmeetlem5  34921  dihmeetlem7N  34923  dihmeetlem10N  34929  dihmeetlem11N  34930  dihmeetlem12N  34931  dihmeetlem13N  34932  dihmeetlem15N  34934  dihmeetlem16N  34935  dihmeetlem17N  34936  dihmeetlem18N  34937  dihmeetlem19N  34938  dihmeetALTN  34940  dih1dimatlem0  34941  dihlspsnssN  34945  dihlspsnat  34946  mapdh8ad  35392  hdmap14lem14  35497  hgmapvvlem3  35541  mzprename  35636  eldioph2lem1  35647  lzunuz  35655  rencldnfi  35709  pellexlem2  35719  infmrgelbi  35769  infmrgelbiOLD  35770  pellfundglb  35778  pellfund14gap  35780  qirropth  35801  rmxycomplete  35810  congadd  35861  acongeq  35878  jm2.19  35893  jm2.23  35896  jm2.20nn  35897  jm2.27  35908  jm3.1  35920  aomclem6  35962  lnmepi  35988  lmhmfgsplit  35989  lmhmlnmsplit  35990  pwssplit4  35992  hbtlem2  36028  hbtlem5  36032  dgraa0p  36060  hashgcdlem  36119  proot1hash  36122  iocunico  36140  relexpxpmin  36354  brtrclfv2  36364  suprnmpt  37477  wessf1ornlem  37497  projf1o  37512  snunioo2  37644  snunioo1  37651  iccintsng  37662  lptre2pt  37758  limcleqr  37763  volioc  37887  iblspltprt  37888  stoweidlem19  37917  stoweidlem20  37918  stoweidlem22  37920  stoweidlem28  37926  stoweidlem34  37933  stoweidlem44  37943  stoweidlem60  37959  wallispilem3  37967  fourierdlem41  38049  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem49  38057  fourierdlem51  38059  fourierdlem54  38062  fourierdlem74  38082  fourierdlem97  38105  caratheodorylem2  38386  ovnsubaddlem2  38431  hspmbllem2  38487  fzopredsuc  38758  iccpartigtl  38775  oexpnegALTV  38844  oexpnegnz  38845  tgblthelfgott  38946  repswpfx  39017  fun2dmnop  39069  fzoopth  39105  1pthond  39859  1pthon2v-av  39868  umgr2wlk  39898  lidldomn1  40194  ofaddmndmap  40398  lincdifsn  40490  lincellss  40492  lincresunit3lem3  40540  islindeps2  40549  lindssnlvec  40552  fdivmptf  40625  refdivmptf  40626