Theorem simpl1 997

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

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 971

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 369  df-3an 973

This theorem is referenced by:  simpll1  1033  simprl1  1039  simp1l1  1087  simp2l1  1093  simp3l1  1099  3anandirs  1329  rspc3ev  3148  brcogw  5084  cocan1  6095  weniso  6151  smogt  6956  smorndom  6957  omeulem1  7149  nnmord  7199  nnmword  7200  difsnen  7518  enfixsn  7545  mapunen  7605  ac6sfi  7679  fipreima  7741  elfiun  7805  ordiso2  7855  wemaplem2  7887  wemapso  7891  en2eqpr  8298  indcardi  8335  fodomfi2  8354  iunfictbso  8408  infmap2  8511  cofsmo  8562  cfsmolem  8563  coftr  8566  fin23lem11  8610  fincssdom  8616  fin23lem26  8618  isf32lem9  8654  ac6num  8772  gchdomtri  8918  gchpwdom  8959  winainflem  8982  tskuni  9072  gruima  9091  gruf  9100  grudomon  9106  elnpi  9277  distrlem4pr  9315  prlem934  9322  addcan  9675  addcan2  9676  ltmul1a  10308  ledivmul2OLD  10339  suprleub  10423  supmul1  10424  infmrgelb  10439  suprzcl  10859  uzsupss  11093  xleadd1a  11366  xlesubadd  11376  xmulasslem3  11399  xlemul2a  11402  xadddilem  11407  xadddi2  11410  ixxun  11466  icoshftf1o  11564  snunioc  11569  lincmb01cmp  11584  iccf1o  11585  fzofzim  11764  ltexp2a  12120  leexp2  12123  ltexp2r  12125  exple1  12128  expnlbnd2  12199  ccatass  12514  ccat2s1fvw  12551  swrdswrdlem  12595  ccatopth  12606  cshco  12713  repsco  12716  s2f1o  12775  limsupgre  13306  addcn2  13418  mulcn2  13420  ntrivcvgmul  13713  dvdsadd2b  14030  dvdsmod  14045  oexpneg  14051  sadass  14123  gcdass  14185  rplpwr  14196  rppwr  14197  coprmdvds2  14246  rpmulgcd2  14248  qredeq  14249  rpexp  14263  rpdvds  14267  prmdiveq  14318  odzdvds  14324  modprmn0modprm0  14334  coprimeprodsq2  14336  pythagtriplem3  14344  pcdvdsb  14394  pcgcd1  14402  qexpz  14422  pockthg  14426  vdwnnlem1  14515  0ram  14540  ramz2  14544  lubss  15868  lubun  15870  clatleglb  15873  clatglbss  15874  mrelatglb  15931  isnsgrp  16032  issubmnd  16065  ress0g  16066  gsumccat  16126  frmdss2  16148  mulgneg  16277  mulgdirlem  16283  submmulg  16294  subgmulg  16332  nmzsubg  16359  ghmmulg  16396  gsmsymgreqlem1  16572  pmtrfb  16607  psgnunilem4  16639  odmodnn0  16681  odnncl  16686  odmod  16687  odmulgid  16693  odmulgeq  16696  odf1o1  16709  odf1o2  16710  odngen  16714  gexdvdsi  16720  pgpfi1  16732  odcau  16741  subgslw  16753  fislw  16762  lsmssv  16780  lsmless1x  16781  lsmless2x  16782  lsmsubm  16790  lsmmod  16810  lsmmod2  16811  efgred  16883  cntzcmn  16965  ghmplusg  16969  odadd1  16971  odadd2  16972  odadd  16973  lsmcomx  16979  gsumconst  17070  srg1zr  17293  ring1eq0  17351  mulgass2  17360  isabvd  17582  lssintcl  17723  0lmhm  17799  lmhmvsca  17804  reslmhm2b  17813  pwssplit1  17818  pwssplit3  17820  lspfixed  17887  lspsnat  17904  lidldvgen  18016  issubassa  18086  evlsval2  18302  psrplusgpropd  18390  coe1subfv  18420  coe1mul2  18423  xrsdsreclblem  18577  regsumsupp  18749  obselocv  18850  uvcresum  18913  frlmsslsp  18916  frlmup4  18921  lindff1  18940  f1lindf  18942  lsslindf  18950  islindf4  18958  lbslcic  18961  mhmvlin  18984  mpt2matmul  19033  mamutpos  19045  scmatscmide  19094  mavmulsolcl  19138  marrepcl  19151  mdetdiag  19186  mdetunilem1  19199  mdetunilem3  19201  mdetunilem7  19205  mdetunilem9  19207  mdetmul  19210  slesolinvbi  19268  m2pmfzmap  19333  pmatcollpwlem  19366  pmatcollpw  19367  mp2pm2mplem4  19395  chpdmatlem3  19426  chfacfisfcpmat  19441  chfacfscmulgsum  19446  chfacfpmmulgsum  19450  chfacfpmmulgsum2  19451  cayhamlem1  19452  cpmidpmatlem2  19457  cpmadugsumlemB  19460  cpmadugsumlemC  19461  cpmadugsumlemF  19462  riinopn  19502  neiint  19691  topssnei  19711  restntr  19769  iscnp4  19850  cnconst2  19870  cnrest2  19873  cnprest2  19877  cnpdis  19880  cnt0  19933  cnt1  19937  cnhaus  19941  ordthauslem  19970  cncmp  19978  fiuncmp  19990  sscmp  19991  hauscmp  19993  cnconn  20008  uncon  20015  nlly2i  20062  llynlly  20063  nllyidm  20075  finlocfin  20106  ptrescn  20225  xkococnlem  20245  qtoptop2  20285  qtopss  20301  kqfvima  20316  r0cld  20324  ordthmeolem  20387  fbssint  20424  fmf  20531  fmss  20532  elfm  20533  rnelfmlem  20538  rnelfm  20539  fmco  20547  flimss2  20558  flimss1  20559  flimrest  20569  flftg  20582  cnpflf2  20586  cnpflf  20587  flfcnp  20590  supnfcls  20606  fclsss1  20608  fclsss2  20609  fcfnei  20621  fcfelbas  20622  cnpfcfi  20626  subgntr  20690  opnsubg  20691  cldsubg  20694  ghmcnp  20698  utop2nei  20838  neipcfilu  20884  bldisj  20986  blgt0  20987  bl2in  20988  blss2ps  20991  blss2  20992  blssps  21012  blss  21013  xmetresbl  21025  lpbl  21091  blcld  21093  stdbdbl  21105  metcnp3  21128  metcnp2  21130  txmetcnp  21135  blval2  21163  nmoix  21321  nmoeq0  21328  icoopnst  21524  iocopnst  21525  xrhmeo  21531  nmhmcn  21688  cphsqrtcl2  21718  cphsqrtcl3  21719  cfil3i  21793  caublcls  21832  bcthlem5  21852  cmetcusp1OLD  21876  cmetcusp1  21877  rrxcph  21909  pjth  21939  ovoliunlem2  21999  volun  22040  volsup2  22099  mbfimaopn2  22149  iblconst  22309  itgconst  22310  dvcnp2  22408  dvcn  22409  deg1mul3le  22602  deg1tmle  22603  dvdsq1p  22646  ig1peu  22657  ig1pdvds  22662  coeid3  22722  dgrmulc  22753  efcvx  22929  tanord  23010  logdivlti  23092  logccv  23131  recxpcl  23143  cxpeq  23218  ang180  23264  isosctrlem2  23269  cxp2lim  23423  amgm  23437  muval1  23524  dvdssqf  23529  mumullem2  23571  mumul  23572  bcmono  23669  lgsfcl2  23694  lgsdilem  23714  lgsdirprm  23721  lgsdir  23722  lgsdi  23724  lgsne0  23725  padicabv  23932  brbtwn2  24329  colinearalglem1  24330  colinearalg  24334  axcgrtr  24339  axsegconlem8  24348  axsegconlem9  24349  axsegconlem10  24350  axcontlem8  24395  axcontlem10  24397  2pthon  24725  clwwlkfo  24918  clwwlkext2edg  24923  erclwwlksym  24935  erclwwlknsym  24947  clwlkfoclwwlk  24966  clwlkf1clwwlklem  24970  numclwwlk2lem1  25223  numclwwlk5  25233  frgraregord13  25240  gxcom  25388  gxnn0add  25393  zerdivemp1  25553  nvmul0or  25664  ipval2lem2  25731  ipval2lem5  25737  lnomul  25792  shless  26394  shlej1  26395  pjspansn  26612  hoadddi  26838  kbmul  26990  homco2  27012  kbass2  27152  eliccelico  27741  elicoelioo  27742  iocinioc2  27743  iocinif  27745  xrge0adddir  27835  xrge0npcan  27837  archiabl  27895  ress1r  27933  rhmdvdsr  27962  pstmfval  28029  fmcncfil  28067  zrhnm  28103  qqhnm  28124  measvunilem  28339  volfiniune  28358  dya2iocnrect  28408  sibfinima  28464  probun  28541  probinc  28543  cndprob01  28557  pconpi1  28871  cvmsss2  28908  mrsubcv  29059  msubvrs  29109  binomrisefac  29330  dvdspw  29341  br6  29352  br4  29353  frrlem4  29555  cgrcomim  29792  cgrtriv  29805  cgrextend  29811  segconeq  29813  btwntriv2  29815  btwnintr  29822  btwnexch3  29823  btwnouttr2  29825  trisegint  29831  cgrsub  29848  cgrxfr  29858  btwnxfr  29859  lineext  29879  btwnconn1lem13  29902  btwnconn1lem14  29903  btwnconn3  29906  segcon2  29908  brsegle  29911  brsegle2  29912  segletr  29917  segleantisym  29918  seglelin  29919  outsideofeu  29934  lineunray  29950  lineelsb2  29951  areacirc  30278  ivthALT  30319  cocanfo  30374  upixp  30386  ismtyima  30465  rrndstprj2  30493  zerdivemp1x  30524  mzprename  30847  eldioph2lem1  30858  lzunuz  30866  rencldnfi  30920  pellexlem2  30931  infmrgelbi  30979  pellfundglb  30986  pellfund14gap  30988  qirropth  31009  rmxycomplete  31018  congadd  31069  acongeq  31086  jm2.19  31101  jm2.23  31104  jm2.20nn  31105  jm2.27  31116  jm3.1  31128  aomclem6  31171  lnmepi  31197  lmhmfgsplit  31198  lmhmlnmsplit  31199  pwssplit4  31201  hbtlem2  31241  hbtlem5  31245  dgraa0p  31266  hashgcdlem  31325  proot1hash  31328  iocunico  31346  lcmass  31386  suprnmpt  31618  snunioo2  31710  snunioo1  31718  iccintsng  31729  lptre2pt  31812  limcleqr  31816  volioc  31937  iblspltprt  31938  stoweidlem19  31967  stoweidlem20  31968  stoweidlem22  31970  stoweidlem28  31976  stoweidlem34  31982  stoweidlem44  31992  stoweidlem60  32008  wallispilem3  32015  fourierdlem41  32096  fourierdlem42  32097  fourierdlem49  32104  fourierdlem51  32106  fourierdlem54  32109  fourierdlem74  32129  fourierdlem97  32152  oexpnegALTV  32519  oexpnegnz  32520  repswpfx  32611  fzoopth  32660  lidldomn1  32927  ofaddmndmap  33133  lincdifsn  33225  lincellss  33227  lincresunit3lem3  33275  islindeps2  33284  lindssnlvec  33287  fdivmptf  33362  refdivmptf  33363  bnj517  34290  bnj594  34317  lsatfixedN  35147  lssat  35154  eqlkr  35237  eqlkr2  35238  lkrlsp  35240  lshpkrlem4  35251  opposet  35319  cvrcon3b  35415  cvrcmp  35421  atlen0  35448  atnle  35455  atlatmstc  35457  cvlatexch3  35476  cvlsupr2  35481  hlsupr2  35524  hlrelat2  35540  cvrexchlem  35556  lnnat  35564  atcvrj2b  35569  atle  35573  atexchcvrN  35577  atbtwn  35583  athgt  35593  3dimlem3  35598  3dim1  35604  1cvratlt  35611  1cvrjat  35612  ps-1  35614  ps-2  35615  3atlem3  35622  3atlem5  35624  3atlem7  35626  llni  35645  llni2  35649  atcvrlln2  35656  llnexatN  35658  llncmp  35659  2llnmat  35661  2at0mat0  35662  lplni  35669  lplnnle2at  35678  2atnelpln  35681  lplnllnneN  35693  llncvrlpln2  35694  2lplnmN  35696  2llnmj  35697  lplncmp  35699  lplnexatN  35700  lplnexllnN  35701  2llnm3N  35706  lvoli  35712  lvoli3  35714  islvol2aN  35729  4atlem0a  35730  4atlem3  35733  4atlem3a  35734  4atlem4a  35736  4atlem4b  35737  4atlem4c  35738  4atlem4d  35739  4atlem10b  35742  4atlem11  35746  4atlem12  35749  lplncvrlvol2  35752  lvolcmp  35754  2lplnmj  35759  islinei  35877  pmapglbx  35906  linepmap  35912  lneq2at  35915  lnjatN  35917  lncvrat  35919  lncmp  35920  2llnma3r  35925  elpaddatriN  35940  elpaddat  35941  paddcom  35950  paddss1  35954  paddss2  35955  paddss12  35956  paddasslem6  35962  paddasslem7  35963  paddasslem8  35964  paddasslem9  35965  paddasslem15  35971  pmodlem2  35984  pmodl42N  35988  pmapjoin  35989  llnmod1i2  35997  2polcon4bN  36055  polcon2bN  36057  poml4N  36090  poml6N  36092  osumcllem1N  36093  osumcllem2N  36094  osumcllem11N  36103  osumclN  36104  pmapojoinN  36105  pexmidlem2N  36108  pexmidlem3N  36109  pexmidlem4N  36110  pexmidlem6N  36112  pexmidlem7N  36113  pl42lem2N  36117  pl42lem3N  36118  pl42lem4N  36119  pl42N  36120  lhpexle2lem  36146  lhpexle3lem  36148  lhpexle3  36149  lhpmcvr3  36162  lhp2at0nle  36172  lhprelat3N  36177  4atex  36213  4atex2  36214  lauteq  36232  lautco  36234  ltrncoidN  36265  ltrneq2  36285  ltrnnidn  36312  ltrnideq  36313  trlnid  36317  ltrnatlw  36321  trlnle  36324  trlval3  36325  trlval4  36326  cdlemc  36335  cdlemd5  36340  cdlemd9  36344  ltrneq3  36346  cdleme0moN  36363  cdleme20  36463  cdleme21j  36475  cdleme21  36476  cdleme27cl  36505  cdlemefrs29bpre0  36535  cdlemefs27cl  36552  cdlemefs32sn1aw  36553  cdleme43fsv1snlem  36559  cdleme32d  36583  cdleme32f  36585  cdleme32le  36586  cdleme35h2  36596  cdleme38n  36603  cdleme40m  36606  cdleme41snaw  36615  cdleme42ke  36624  cdleme17d3  36635  cdleme48fvg  36639  cdlemeg46fvcl  36645  cdlemeg46fgN  36673  cdleme48gfv1  36675  cdleme48fgv  36677  cdleme50trn3  36692  trlord  36708  ltrniotavalbN  36723  cdlemb3  36745  cdlemg6c  36759  cdlemg6  36762  cdlemg7N  36765  cdlemg8c  36768  cdlemg8  36770  cdlemg11a  36776  cdlemg11b  36781  cdlemg12e  36786  cdlemg15a  36794  cdlemg15  36795  cdlemg16  36796  cdlemg16z  36798  cdlemg16zz  36799  cdlemg17dN  36802  cdlemg18a  36817  cdlemg20  36824  cdlemg22  36826  cdlemg24  36827  cdlemg37  36828  cdlemg31d  36839  cdlemg29  36844  cdlemg33b  36846  cdlemg33  36850  cdlemg38  36854  cdlemg39  36855  cdlemg40  36856  trlco  36866  trlcone  36867  cdlemg42  36868  cdlemg44b  36871  ltrncom  36877  trljco  36879  tendococl  36911  tendoplcl  36920  tendoplcom  36921  cdlemj2  36961  cdlemj3  36962  tendoid0  36964  tendoconid  36968  tendotr  36969  cdlemk25-3  37043  cdlemk26b-3  37044  cdlemk34  37049  cdlemk36  37052  cdlemk38  37054  cdlemkid4  37073  cdlemk35s-id  37077  cdlemk39s-id  37079  cdlemk19x  37082  cdlemk53  37096  cdlemk55  37100  cdlemk55u  37105  cdlemk39u  37107  cdlemk19u  37109  cdlemk56  37110  tendoex  37114  cdleml3N  37117  cdleml5N  37119  tendospcanN  37163  cdlemm10N  37258  cdlemn11pre  37350  dihord2pre  37365  dihvalcqpre  37375  dihopelvalcpre  37388  dihord6apre  37396  dihord5b  37399  dihord5apre  37402  dihord  37404  dihmeetlem1N  37430  dihglblem5apreN  37431  dihglblem3N  37435  dihmeetlem2N  37439  dihglbcpreN  37440  dihmeetbN  37443  dihmeetlem4preN  37446  dihmeetlem5  37448  dihmeetlem7N  37450  dihmeetlem10N  37456  dihmeetlem11N  37457  dihmeetlem12N  37458  dihmeetlem13N  37459  dihmeetlem15N  37461  dihmeetlem16N  37462  dihmeetlem17N  37463  dihmeetlem18N  37464  dihmeetlem19N  37465  dihmeetALTN  37467  dih1dimatlem0  37468  dihlspsnssN  37472  dihlspsnat  37473  mapdh8ad  37919  hdmap14lem14  38024  hgmapvvlem3  38068  relexpxpmin  38244  brtrclfv2  38258