Theorem simpl1 991

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

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

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 967

This theorem is referenced by:  simpll1  1027  simprl1  1033  simp1l1  1081  simp2l1  1087  simp3l1  1093  3anandirs  1322  rspc3ev  3188  brcogw  5115  cocan1  6103  weniso  6153  smogt  6937  smorndom  6938  omeulem1  7130  nnmord  7180  nnmword  7181  difsnen  7502  enfixsn  7529  mapunen  7589  ac6sfi  7666  fipreima  7727  elfiun  7790  ordiso2  7839  wemaplem2  7871  wemapso  7875  en2eqpr  8284  indcardi  8321  fodomfi2  8340  iunfictbso  8394  infmap2  8497  cofsmo  8548  cfsmolem  8549  coftr  8552  fin23lem11  8596  fincssdom  8602  fin23lem26  8604  isf32lem9  8640  ac6num  8758  gchdomtri  8906  gchpwdom  8947  winainflem  8970  tskuni  9060  gruima  9079  gruf  9088  grudomon  9094  elnpi  9267  distrlem4pr  9305  prlem934  9312  addcan  9663  addcan2  9664  ltmul1a  10288  ledivmulOLD  10316  ledivmul2OLD  10320  suprleub  10404  supmul1  10405  infmrgelb  10420  suprzcl  10831  uzsupss  11057  xleadd1a  11326  xlesubadd  11336  xmulasslem3  11359  xlemul2a  11362  xadddilem  11367  xadddi2  11370  ixxun  11426  icoshftf1o  11524  snunioc  11529  lincmb01cmp  11544  iccf1o  11545  fzofzim  11709  ltexp2a  12031  leexp2  12034  ltexp2r  12036  exple1  12039  expnlbnd2  12111  ccatass  12403  swrdswrdlem  12470  ccatopth  12481  cshco  12581  repsco  12584  s2f1o  12643  limsupgre  13076  addcn2  13188  mulcn2  13190  dvdsadd2b  13692  dvdsmod  13707  oexpneg  13712  gcdass  13846  rplpwr  13857  rppwr  13858  coprmdvds2  13906  rpmulgcd2  13908  qredeq  13909  rpexp  13923  rpdvds  13927  prmdiveq  13978  odzdvds  13984  modprmn0modprm0  13992  coprimeprodsq2  13994  pythagtriplem3  14002  pcdvdsb  14052  pcgcd1  14060  qexpz  14080  pockthg  14084  vdwnnlem1  14173  0ram  14198  ramz2  14202  lubss  15409  lubun  15411  clatleglb  15414  clatglbss  15415  mrelatglb  15472  issubmnd  15567  ress0g  15568  gsumccat  15637  frmdss2  15659  mulgneg  15763  mulgdirlem  15769  submmulg  15780  subgmulg  15813  nmzsubg  15840  ghmmulg  15877  gsmsymgreqlem1  16053  pmtrfb  16089  psgnunilem4  16121  odmodnn0  16163  odnncl  16168  odmod  16169  odmulgid  16175  odmulgeq  16178  odf1o1  16191  odf1o2  16192  odngen  16196  gexdvdsi  16202  pgpfi1  16214  odcau  16223  subgslw  16235  fislw  16244  lsmssv  16262  lsmless1x  16263  lsmless2x  16264  lsmsubm  16272  lsmmod  16292  lsmmod2  16293  efgred  16365  cntzcmn  16444  ghmplusg  16448  odadd1  16450  odadd2  16451  odadd  16452  lsmcomx  16458  gsumconst  16548  rng1eq0  16806  mulgass2  16814  isabvd  17027  lssintcl  17167  0lmhm  17243  lmhmvsca  17248  reslmhm2b  17257  pwssplit1  17262  pwssplit3  17264  lspfixed  17331  lspsnat  17348  lidldvgen  17459  issubassa  17517  evlsval2  17729  psrplusgpropd  17813  coe1subfv  17842  coe1mul2  17845  xrsdsreclblem  17983  regsumsupp  18176  obselocv  18277  uvcresum  18342  frlmsslsp  18347  frlmsslspOLD  18348  frlmup4  18353  lindff1  18373  f1lindf  18375  lsslindf  18383  islindf4  18391  lbslcic  18394  mhmvlin  18421  mamutpos  18469  mavmulsolcl  18488  marrepcl  18501  mdetdiag  18536  mdetunilem1  18549  mdetunilem3  18551  mdetunilem7  18555  mdetunilem9  18557  mdetmul  18560  slesolinvbi  18618  riinopn  18652  neiint  18839  topssnei  18859  restntr  18917  iscnp4  18998  cnconst2  19018  cnrest2  19021  cnprest2  19025  cnpdis  19028  cnt0  19081  cnt1  19085  cnhaus  19089  ordthauslem  19118  cncmp  19126  fiuncmp  19138  sscmp  19139  hauscmp  19141  cnconn  19157  uncon  19164  nlly2i  19211  llynlly  19212  nllyidm  19224  ptrescn  19343  xkococnlem  19363  qtoptop2  19403  qtopss  19419  kqfvima  19434  r0cld  19442  ordthmeolem  19505  fbssint  19542  fmf  19649  fmss  19650  elfm  19651  rnelfmlem  19656  rnelfm  19657  fmco  19665  flimss2  19676  flimss1  19677  flimrest  19687  flftg  19700  cnpflf2  19704  cnpflf  19705  flfcnp  19708  supnfcls  19724  fclsss1  19726  fclsss2  19727  fcfnei  19739  fcfelbas  19740  cnpfcfi  19744  subgntr  19808  opnsubg  19809  cldsubg  19812  ghmcnp  19816  utop2nei  19956  neipcfilu  20002  bldisj  20104  blgt0  20105  bl2in  20106  blss2ps  20109  blss2  20110  blssps  20130  blss  20131  xmetresbl  20143  lpbl  20209  blcld  20211  stdbdbl  20223  metcnp3  20246  metcnp2  20248  txmetcnp  20253  blval2  20281  nmoix  20439  nmoeq0  20446  icoopnst  20642  iocopnst  20643  xrhmeo  20649  nmhmcn  20806  cphsqrcl2  20836  cphsqrcl3  20837  cfil3i  20911  caublcls  20950  bcthlem5  20970  cmetcusp1OLD  20994  cmetcusp1  20995  rrxcph  21027  pjth  21057  ovoliunlem2  21117  volun  21158  volsup2  21217  mbfimaopn2  21267  iblconst  21427  itgconst  21428  dvcnp2  21526  dvcn  21527  deg1mul3le  21720  deg1tmle  21721  dvdsq1p  21764  ig1peu  21775  ig1pdvds  21780  coeid3  21840  dgrmulc  21870  efcvx  22046  tanord  22126  logdivlti  22201  logccv  22240  recxpcl  22252  cxpeq  22327  ang180  22342  isosctrlem2  22349  cxp2lim  22502  amgm  22516  muval1  22603  dvdssqf  22608  mumullem2  22650  mumul  22651  bcmono  22748  lgsfcl2  22773  lgsdilem  22793  lgsdirprm  22800  lgsdir  22801  lgsdi  22803  lgsne0  22804  brbtwn2  23302  colinearalglem1  23303  colinearalg  23307  axcgrtr  23312  axsegconlem8  23321  axsegconlem9  23322  axsegconlem10  23323  axcontlem8  23368  axcontlem10  23370  2pthon  23652  gxcom  23907  gxnn0add  23912  zerdivemp1  24072  nvmul0or  24183  ipval2lem2  24250  ipval2lem5  24256  lnomul  24311  shless  24913  shlej1  24914  pjspansn  25131  hoadddi  25358  kbmul  25510  homco2  25532  kbass2  25672  eliccelico  26211  elicoelioo  26212  iocinioc2  26213  iocinif  26215  xrge0adddir  26299  xrge0npcan  26301  archiabl  26359  ress1r  26401  rhmdvdsr  26430  pstmfval  26467  fmcncfil  26505  zrhnm  26542  qqhnm  26563  measvunilem  26770  volfiniune  26789  dya2iocnrect  26839  sibfinima  26868  probun  26945  probinc  26947  cndprob01  26961  signswmnd  27101  pconpi1  27269  cvmsss2  27306  ntrivcvgmul  27560  binomrisefac  27688  dvdspw  27699  br6  27710  br4  27711  frrlem4  27914  cgrcomim  28163  cgrtriv  28176  cgrextend  28182  segconeq  28184  btwntriv2  28186  btwnintr  28193  btwnexch3  28194  btwnouttr2  28196  trisegint  28202  cgrsub  28219  cgrxfr  28229  btwnxfr  28230  lineext  28250  btwnconn1lem13  28273  btwnconn1lem14  28274  btwnconn3  28277  segcon2  28279  brsegle  28282  brsegle2  28283  segletr  28288  segleantisym  28289  seglelin  28290  outsideofeu  28305  lineunray  28321  lineelsb2  28322  areacirc  28636  ivthALT  28677  finlocfin  28718  cocanfo  28758  upixp  28770  ismtyima  28849  rrndstprj2  28877  zerdivemp1x  28908  mzprename  29233  eldioph2lem1  29245  lzunuz  29253  rencldnfi  29307  pellexlem2  29318  infmrgelbi  29366  pellfundglb  29373  pellfund14gap  29375  qirropth  29396  rmxycomplete  29405  congadd  29456  acongeq  29473  jm2.19  29489  jm2.23  29492  jm2.20nn  29493  jm2.27  29504  jm3.1  29516  aomclem6  29559  lnmepi  29585  lmhmfgsplit  29586  lmhmlnmsplit  29587  pwssplit4  29589  hbtlem2  29627  hbtlem5  29631  dgraa0p  29653  hashgcdlem  29712  proot1hash  29715  iocunico  29733  stoweidlem19  29961  stoweidlem20  29962  stoweidlem22  29964  stoweidlem28  29970  stoweidlem34  29976  stoweidlem44  29986  stoweidlem60  30002  wallispilem3  30009  fzoopth  30360  clwwlkfo  30606  clwwlkext2edg  30611  erclwwlksym  30631  erclwwlknsym  30647  clwlkfoclwwlk  30665  clwlkf1clwwlklem  30669  numclwwlk2lem1  30842  numclwwlk5  30852  frgraregord13  30859  ofaddmndmap  30881  scmatel  31021  lincdifsn  31076  lincellss  31078  lincresunit3lem3  31126  islindeps2  31135  lindssnlvec  31138  m2pmfzmap  31230  pmatcollpwlem  31253  pmatcollpw  31254  pmatcollpw3  31256  mp2pm2mplem4  31281  cpdmatlem3  31311  chfacfisfcpmat  31326  chfacfscmulgsum  31331  chfacfpmmulgsum  31335  chfacfpmmulgsum2  31336  cayhamlem1  31337  cpmidpmatlem2  31342  cpmadugsumlemB  31345  cpmadugsumlemC  31346  cpmadugsumlemF  31347  cpmadumatpolylem3  31354  bnj517  32195  bnj594  32222  lsatfixedN  32977  lssat  32984  eqlkr  33067  eqlkr2  33068  lkrlsp  33070  lshpkrlem4  33081  opposet  33149  cvrcon3b  33245  cvrcmp  33251  atlen0  33278  atnle  33285  atlatmstc  33287  cvlatexch3  33306  cvlsupr2  33311  hlsupr2  33354  hlrelat2  33370  cvrexchlem  33386  lnnat  33394  atcvrj2b  33399  atle  33403  atexchcvrN  33407  atbtwn  33413  athgt  33423  3dimlem3  33428  3dim1  33434  1cvratlt  33441  1cvrjat  33442  ps-1  33444  ps-2  33445  3atlem3  33452  3atlem5  33454  3atlem7  33456  llni  33475  llni2  33479  atcvrlln2  33486  llnexatN  33488  llncmp  33489  2llnmat  33491  2at0mat0  33492  lplni  33499  lplnnle2at  33508  2atnelpln  33511  lplnllnneN  33523  llncvrlpln2  33524  2lplnmN  33526  2llnmj  33527  lplncmp  33529  lplnexatN  33530  lplnexllnN  33531  2llnm3N  33536  lvoli  33542  lvoli3  33544  islvol2aN  33559  4atlem0a  33560  4atlem3  33563  4atlem3a  33564  4atlem4a  33566  4atlem4b  33567  4atlem4c  33568  4atlem4d  33569  4atlem10b  33572  4atlem11  33576  4atlem12  33579  lplncvrlvol2  33582  lvolcmp  33584  2lplnmj  33589  islinei  33707  pmapglbx  33736  linepmap  33742  lneq2at  33745  lnjatN  33747  lncvrat  33749  lncmp  33750  2llnma3r  33755  elpaddatriN  33770  elpaddat  33771  paddcom  33780  paddss1  33784  paddss2  33785  paddss12  33786  paddasslem6  33792  paddasslem7  33793  paddasslem8  33794  paddasslem9  33795  paddasslem15  33801  pmodlem2  33814  pmodl42N  33818  pmapjoin  33819  llnmod1i2  33827  2polcon4bN  33885  polcon2bN  33887  poml4N  33920  poml6N  33922  osumcllem1N  33923  osumcllem2N  33924  osumcllem11N  33933  osumclN  33934  pmapojoinN  33935  pexmidlem2N  33938  pexmidlem3N  33939  pexmidlem4N  33940  pexmidlem6N  33942  pexmidlem7N  33943  pl42lem2N  33947  pl42lem3N  33948  pl42lem4N  33949  pl42N  33950  lhpexle2lem  33976  lhpexle3lem  33978  lhpexle3  33979  lhpmcvr3  33992  lhp2at0nle  34002  lhprelat3N  34007  4atex  34043  4atex2  34044  lauteq  34062  lautco  34064  ltrncoidN  34095  ltrneq2  34115  ltrnnidn  34141  ltrnideq  34142  trlnid  34146  ltrnatlw  34150  trlnle  34153  trlval3  34154  trlval4  34155  cdlemc  34164  cdlemd5  34169  cdlemd9  34173  ltrneq3  34175  cdleme0moN  34192  cdleme20  34291  cdleme21j  34303  cdleme21  34304  cdleme27cl  34333  cdlemefrs29bpre0  34363  cdlemefs27cl  34380  cdlemefs32sn1aw  34381  cdleme43fsv1snlem  34387  cdleme32d  34411  cdleme32f  34413  cdleme32le  34414  cdleme35h2  34424  cdleme38n  34431  cdleme40m  34434  cdleme41snaw  34443  cdleme42ke  34452  cdleme17d3  34463  cdleme48fvg  34467  cdlemeg46fvcl  34473  cdlemeg46fgN  34501  cdleme48gfv1  34503  cdleme48fgv  34505  cdleme50trn3  34520  trlord  34536  ltrniotavalbN  34551  cdlemb3  34573  cdlemg6c  34587  cdlemg6  34590  cdlemg7N  34593  cdlemg8c  34596  cdlemg8  34598  cdlemg11a  34604  cdlemg11b  34609  cdlemg12e  34614  cdlemg15a  34622  cdlemg15  34623  cdlemg16  34624  cdlemg16z  34626  cdlemg16zz  34627  cdlemg17dN  34630  cdlemg18a  34645  cdlemg20  34652  cdlemg22  34654  cdlemg24  34655  cdlemg37  34656  cdlemg31d  34667  cdlemg29  34672  cdlemg33b  34674  cdlemg33  34678  cdlemg38  34682  cdlemg39  34683  cdlemg40  34684  trlco  34694  trlcone  34695  cdlemg42  34696  cdlemg44b  34699  ltrncom  34705  trljco  34707  tendococl  34739  tendoplcl  34748  tendoplcom  34749  cdlemj2  34789  cdlemj3  34790  tendoid0  34792  tendoconid  34796  tendotr  34797  cdlemk25-3  34871  cdlemk26b-3  34872  cdlemk34  34877  cdlemk36  34880  cdlemk38  34882  cdlemkid4  34901  cdlemk35s-id  34905  cdlemk39s-id  34907  cdlemk19x  34910  cdlemk53  34924  cdlemk55  34928  cdlemk55u  34933  cdlemk39u  34935  cdlemk19u  34937  cdlemk56  34938  tendoex  34942  cdleml3N  34945  cdleml5N  34947  tendospcanN  34991  cdlemm10N  35086  cdlemn11pre  35178  dihord2pre  35193  dihvalcqpre  35203  dihopelvalcpre  35216  dihord6apre  35224  dihord5b  35227  dihord5apre  35230  dihord  35232  dihmeetlem1N  35258  dihglblem5apreN  35259  dihglblem3N  35263  dihmeetlem2N  35267  dihglbcpreN  35268  dihmeetbN  35271  dihmeetlem4preN  35274  dihmeetlem5  35276  dihmeetlem7N  35278  dihmeetlem10N  35284  dihmeetlem11N  35285  dihmeetlem12N  35286  dihmeetlem13N  35287  dihmeetlem15N  35289  dihmeetlem16N  35290  dihmeetlem17N  35291  dihmeetlem18N  35292  dihmeetlem19N  35293  dihmeetALTN  35295  dih1dimatlem0  35296  dihlspsnssN  35300  dihlspsnat  35301  mapdh8ad  35747  hdmap14lem14  35852  hgmapvvlem3  35896