Theorem simpl1 986

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

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

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 962

This theorem is referenced by:  simpll1  1022  simprl1  1028  simp1l1  1076  simp2l1  1082  simp3l1  1088  3anandirs  1316  rspc3ev  3074  brcogw  4997  cocan1  5984  weniso  6034  smogt  6816  smorndom  6817  omeulem1  7011  nnmord  7061  nnmword  7062  difsnen  7383  enfixsn  7410  mapunen  7470  ac6sfi  7546  fipreima  7607  elfiun  7670  ordiso2  7719  wemaplem2  7751  wemapso  7755  en2eqpr  8164  indcardi  8201  fodomfi2  8220  iunfictbso  8274  infmap2  8377  cofsmo  8428  cfsmolem  8429  coftr  8432  fin23lem11  8476  fincssdom  8482  fin23lem26  8484  isf32lem9  8520  ac6num  8638  gchdomtri  8786  gchpwdom  8827  winainflem  8850  tskuni  8940  gruima  8959  gruf  8968  grudomon  8974  elnpi  9147  distrlem4pr  9185  prlem934  9192  addcan  9543  addcan2  9544  ltmul1a  10168  ledivmulOLD  10196  ledivmul2OLD  10200  suprleub  10284  supmul1  10285  infmrgelb  10300  suprzcl  10711  uzsupss  10937  xleadd1a  11206  xlesubadd  11216  xmulasslem3  11239  xlemul2a  11242  xadddilem  11247  xadddi2  11250  ixxun  11306  icoshftf1o  11397  snunioc  11402  lincmb01cmp  11417  iccf1o  11418  fzofzim  11579  ltexp2a  11901  leexp2  11904  ltexp2r  11906  exple1  11909  expnlbnd2  11981  ccatass  12272  swrdswrdlem  12339  ccatopth  12350  cshco  12450  repsco  12453  s2f1o  12512  limsupgre  12945  addcn2  13057  mulcn2  13059  dvdsadd2b  13560  dvdsmod  13575  oexpneg  13580  gcdass  13714  rplpwr  13725  rppwr  13726  coprmdvds2  13774  rpmulgcd2  13776  qredeq  13777  rpexp  13791  rpdvds  13795  prmdiveq  13846  odzdvds  13852  modprmn0modprm0  13860  coprimeprodsq2  13862  pythagtriplem3  13870  pcdvdsb  13920  pcgcd1  13928  qexpz  13948  pockthg  13952  vdwnnlem1  14041  0ram  14066  ramz2  14070  lubss  15276  lubun  15278  clatleglb  15281  clatglbss  15282  mrelatglb  15339  issubmnd  15434  ress0g  15435  gsumccat  15501  frmdss2  15523  mulgneg  15627  mulgdirlem  15633  submmulg  15644  subgmulg  15677  nmzsubg  15704  ghmmulg  15741  gsmsymgreqlem1  15917  pmtrfb  15953  psgnunilem4  15985  odmodnn0  16025  odnncl  16030  odmod  16031  odmulgid  16037  odmulgeq  16040  odf1o1  16053  odf1o2  16054  odngen  16058  gexdvdsi  16064  pgpfi1  16076  odcau  16085  subgslw  16097  fislw  16106  lsmssv  16124  lsmless1x  16125  lsmless2x  16126  lsmsubm  16134  lsmmod  16154  lsmmod2  16155  efgred  16227  cntzcmn  16306  ghmplusg  16310  odadd1  16312  odadd2  16313  odadd  16314  lsmcomx  16320  gsumconst  16408  rng1eq0  16621  mulgass2  16629  isabvd  16831  lssintcl  16969  0lmhm  17045  lmhmvsca  17050  reslmhm2b  17059  pwssplit1  17064  pwssplit3  17066  lspfixed  17133  lspsnat  17150  lidldvgen  17261  issubassa  17319  psrplusgpropd  17590  coe1subfv  17620  coe1mul2  17623  xrsdsreclblem  17705  regsumsupp  17896  obselocv  17997  uvcresum  18062  frlmsslsp  18067  frlmsslspOLD  18068  frlmup4  18073  lindff1  18093  f1lindf  18095  lsslindf  18103  islindf4  18111  lbslcic  18114  mhmvlin  18141  mamutpos  18187  mavmulsolcl  18206  marrepcl  18219  mdetunilem1  18262  mdetunilem3  18264  mdetunilem7  18268  mdetunilem9  18270  mdetmul  18273  slesolinvbi  18331  riinopn  18365  neiint  18552  topssnei  18572  restntr  18630  iscnp4  18711  cnconst2  18731  cnrest2  18734  cnprest2  18738  cnpdis  18741  cnt0  18794  cnt1  18798  cnhaus  18802  ordthauslem  18831  cncmp  18839  fiuncmp  18851  sscmp  18852  hauscmp  18854  cnconn  18870  uncon  18877  nlly2i  18924  llynlly  18925  nllyidm  18937  ptrescn  19056  xkococnlem  19076  qtoptop2  19116  qtopss  19132  kqfvima  19147  r0cld  19155  ordthmeolem  19218  fbssint  19255  fmf  19362  fmss  19363  elfm  19364  rnelfmlem  19369  rnelfm  19370  fmco  19378  flimss2  19389  flimss1  19390  flimrest  19400  flftg  19413  cnpflf2  19417  cnpflf  19418  flfcnp  19421  supnfcls  19437  fclsss1  19439  fclsss2  19440  fcfnei  19452  fcfelbas  19453  cnpfcfi  19457  subgntr  19521  opnsubg  19522  cldsubg  19525  ghmcnp  19529  utop2nei  19669  neipcfilu  19715  bldisj  19817  blgt0  19818  bl2in  19819  blss2ps  19822  blss2  19823  blssps  19843  blss  19844  xmetresbl  19856  lpbl  19922  blcld  19924  stdbdbl  19936  metcnp3  19959  metcnp2  19961  txmetcnp  19966  blval2  19994  nmoix  20152  nmoeq0  20159  icoopnst  20355  iocopnst  20356  xrhmeo  20362  nmhmcn  20519  cphsqrcl2  20549  cphsqrcl3  20550  cfil3i  20624  caublcls  20663  bcthlem5  20683  cmetcusp1OLD  20707  cmetcusp1  20708  rrxcph  20740  pjth  20770  ovoliunlem2  20830  volun  20870  volsup2  20929  mbfimaopn2  20979  iblconst  21139  itgconst  21140  dvcnp2  21238  dvcn  21239  evlsval2  21374  deg1mul3le  21475  deg1tmle  21476  dvdsq1p  21519  ig1peu  21530  ig1pdvds  21535  coeid3  21595  dgrmulc  21625  efcvx  21801  tanord  21881  logdivlti  21956  logccv  21995  recxpcl  22007  cxpeq  22082  ang180  22097  isosctrlem2  22104  cxp2lim  22257  amgm  22271  muval1  22358  dvdssqf  22363  mumullem2  22405  mumul  22406  bcmono  22503  lgsfcl2  22528  lgsdilem  22548  lgsdirprm  22555  lgsdir  22556  lgsdi  22558  lgsne0  22559  brbtwn2  22976  colinearalglem1  22977  colinearalg  22981  axcgrtr  22986  axsegconlem8  22995  axsegconlem9  22996  axsegconlem10  22997  axcontlem8  23042  axcontlem10  23044  2pthon  23326  gxcom  23581  gxnn0add  23586  zerdivemp1  23746  nvmul0or  23857  ipval2lem2  23924  ipval2lem5  23930  lnomul  23985  shless  24587  shlej1  24588  pjspansn  24805  hoadddi  25032  kbmul  25184  homco2  25206  kbass2  25346  eliccelico  25892  elicoelioo  25893  iocinioc2  25894  iocinif  25896  xrge0adddir  25981  xrge0npcan  25983  archiabl  26041  ress1r  26112  rhmdvdsr  26141  pstmfval  26179  fmcncfil  26217  zrhnm  26254  qqhnm  26275  measvunilem  26482  volfiniune  26502  dya2iocnrect  26552  sibfinima  26575  probun  26652  probinc  26654  cndprob01  26668  signswmnd  26808  pconpi1  26976  cvmsss2  27013  ntrivcvgmul  27266  binomrisefac  27394  dvdspw  27405  br6  27416  br4  27417  frrlem4  27620  cgrcomim  27869  cgrtriv  27882  cgrextend  27888  segconeq  27890  btwntriv2  27892  btwnintr  27899  btwnexch3  27900  btwnouttr2  27902  trisegint  27908  cgrsub  27925  cgrxfr  27935  btwnxfr  27936  lineext  27956  btwnconn1lem13  27979  btwnconn1lem14  27980  btwnconn3  27983  segcon2  27985  brsegle  27988  brsegle2  27989  segletr  27994  segleantisym  27995  seglelin  27996  outsideofeu  28011  lineunray  28027  lineelsb2  28028  areacirc  28335  ivthALT  28376  finlocfin  28417  cocanfo  28457  upixp  28469  ismtyima  28548  rrndstprj2  28576  zerdivemp1x  28607  mzprename  28933  eldioph2lem1  28945  lzunuz  28953  rencldnfi  29007  pellexlem2  29018  infmrgelbi  29066  pellfundglb  29073  pellfund14gap  29075  qirropth  29096  rmxycomplete  29105  congadd  29156  acongeq  29173  jm2.19  29189  jm2.23  29192  jm2.20nn  29193  jm2.27  29204  jm3.1  29216  aomclem6  29259  lnmepi  29285  lmhmfgsplit  29286  lmhmlnmsplit  29287  pwssplit4  29289  hbtlem2  29327  hbtlem5  29331  dgraa0p  29353  hashgcdlem  29412  proot1hash  29415  iocunico  29433  stoweidlem19  29662  stoweidlem20  29663  stoweidlem22  29665  stoweidlem28  29671  stoweidlem34  29677  stoweidlem44  29687  stoweidlem60  29703  wallispilem3  29710  fzoopth  30061  clwwlkfo  30307  clwwlkext2edg  30312  erclwwlksym  30332  erclwwlknsym  30348  clwlkfoclwwlk  30366  clwlkf1clwwlklem  30370  numclwwlk2lem1  30543  numclwwlk5  30553  frgraregord13  30560  ofaddmndmap  30581  mdetdiag  30685  lincdifsn  30707  lincellss  30709  lincresunit3lem3  30757  islindeps2  30766  lindssnlvec  30769  bnj517  31620  bnj594  31647  lsatfixedN  32267  lssat  32274  eqlkr  32357  eqlkr2  32358  lkrlsp  32360  lshpkrlem4  32371  opposet  32439  cvrcon3b  32535  cvrcmp  32541  atlen0  32568  atnle  32575  atlatmstc  32577  cvlatexch3  32596  cvlsupr2  32601  hlsupr2  32644  hlrelat2  32660  cvrexchlem  32676  lnnat  32684  atcvrj2b  32689  atle  32693  atexchcvrN  32697  atbtwn  32703  athgt  32713  3dimlem3  32718  3dim1  32724  1cvratlt  32731  1cvrjat  32732  ps-1  32734  ps-2  32735  3atlem3  32742  3atlem5  32744  3atlem7  32746  llni  32765  llni2  32769  atcvrlln2  32776  llnexatN  32778  llncmp  32779  2llnmat  32781  2at0mat0  32782  lplni  32789  lplnnle2at  32798  2atnelpln  32801  lplnllnneN  32813  llncvrlpln2  32814  2lplnmN  32816  2llnmj  32817  lplncmp  32819  lplnexatN  32820  lplnexllnN  32821  2llnm3N  32826  lvoli  32832  lvoli3  32834  islvol2aN  32849  4atlem0a  32850  4atlem3  32853  4atlem3a  32854  4atlem4a  32856  4atlem4b  32857  4atlem4c  32858  4atlem4d  32859  4atlem10b  32862  4atlem11  32866  4atlem12  32869  lplncvrlvol2  32872  lvolcmp  32874  2lplnmj  32879  islinei  32997  pmapglbx  33026  linepmap  33032  lneq2at  33035  lnjatN  33037  lncvrat  33039  lncmp  33040  2llnma3r  33045  elpaddatriN  33060  elpaddat  33061  paddcom  33070  paddss1  33074  paddss2  33075  paddss12  33076  paddasslem6  33082  paddasslem7  33083  paddasslem8  33084  paddasslem9  33085  paddasslem15  33091  pmodlem2  33104  pmodl42N  33108  pmapjoin  33109  llnmod1i2  33117  2polcon4bN  33175  polcon2bN  33177  poml4N  33210  poml6N  33212  osumcllem1N  33213  osumcllem2N  33214  osumcllem11N  33223  osumclN  33224  pmapojoinN  33225  pexmidlem2N  33228  pexmidlem3N  33229  pexmidlem4N  33230  pexmidlem6N  33232  pexmidlem7N  33233  pl42lem2N  33237  pl42lem3N  33238  pl42lem4N  33239  pl42N  33240  lhpexle2lem  33266  lhpexle3lem  33268  lhpexle3  33269  lhpmcvr3  33282  lhp2at0nle  33292  lhprelat3N  33297  4atex  33333  4atex2  33334  lauteq  33352  lautco  33354  ltrncoidN  33385  ltrneq2  33405  ltrnnidn  33431  ltrnideq  33432  trlnid  33436  ltrnatlw  33440  trlnle  33443  trlval3  33444  trlval4  33445  cdlemc  33454  cdlemd5  33459  cdlemd9  33463  ltrneq3  33465  cdleme0moN  33482  cdleme20  33581  cdleme21j  33593  cdleme21  33594  cdleme27cl  33623  cdlemefrs29bpre0  33653  cdlemefs27cl  33670  cdlemefs32sn1aw  33671  cdleme43fsv1snlem  33677  cdleme32d  33701  cdleme32f  33703  cdleme32le  33704  cdleme35h2  33714  cdleme38n  33721  cdleme40m  33724  cdleme41snaw  33733  cdleme42ke  33742  cdleme17d3  33753  cdleme48fvg  33757  cdlemeg46fvcl  33763  cdlemeg46fgN  33791  cdleme48gfv1  33793  cdleme48fgv  33795  cdleme50trn3  33810  trlord  33826  ltrniotavalbN  33841  cdlemb3  33863  cdlemg6c  33877  cdlemg6  33880  cdlemg7N  33883  cdlemg8c  33886  cdlemg8  33888  cdlemg11a  33894  cdlemg11b  33899  cdlemg12e  33904  cdlemg15a  33912  cdlemg15  33913  cdlemg16  33914  cdlemg16z  33916  cdlemg16zz  33917  cdlemg17dN  33920  cdlemg18a  33935  cdlemg20  33942  cdlemg22  33944  cdlemg24  33945  cdlemg37  33946  cdlemg31d  33957  cdlemg29  33962  cdlemg33b  33964  cdlemg33  33968  cdlemg38  33972  cdlemg39  33973  cdlemg40  33974  trlco  33984  trlcone  33985  cdlemg42  33986  cdlemg44b  33989  ltrncom  33995  trljco  33997  tendococl  34029  tendoplcl  34038  tendoplcom  34039  cdlemj2  34079  cdlemj3  34080  tendoid0  34082  tendoconid  34086  tendotr  34087  cdlemk25-3  34161  cdlemk26b-3  34162  cdlemk34  34167  cdlemk36  34170  cdlemk38  34172  cdlemkid4  34191  cdlemk35s-id  34195  cdlemk39s-id  34197  cdlemk19x  34200  cdlemk53  34214  cdlemk55  34218  cdlemk55u  34223  cdlemk39u  34225  cdlemk19u  34227  cdlemk56  34228  tendoex  34232  cdleml3N  34235  cdleml5N  34237  tendospcanN  34281  cdlemm10N  34376  cdlemn11pre  34468  dihord2pre  34483  dihvalcqpre  34493  dihopelvalcpre  34506  dihord6apre  34514  dihord5b  34517  dihord5apre  34520  dihord  34522  dihmeetlem1N  34548  dihglblem5apreN  34549  dihglblem3N  34553  dihmeetlem2N  34557  dihglbcpreN  34558  dihmeetbN  34561  dihmeetlem4preN  34564  dihmeetlem5  34566  dihmeetlem7N  34568  dihmeetlem10N  34574  dihmeetlem11N  34575  dihmeetlem12N  34576  dihmeetlem13N  34577  dihmeetlem15N  34579  dihmeetlem16N  34580  dihmeetlem17N  34581  dihmeetlem18N  34582  dihmeetlem19N  34583  dihmeetALTN  34585  dih1dimatlem0  34586  dihlspsnssN  34590  dihlspsnat  34591  mapdh8ad  35037  hdmap14lem14  35142  hgmapvvlem3  35186