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  1321  rspc3ev  3078  brcogw  5003  cocan1  5990  weniso  6040  smogt  6820  smorndom  6821  omeulem1  7013  nnmord  7063  nnmword  7064  difsnen  7385  enfixsn  7412  mapunen  7472  ac6sfi  7548  fipreima  7609  elfiun  7672  ordiso2  7721  wemaplem2  7753  wemapso  7757  en2eqpr  8166  indcardi  8203  fodomfi2  8222  iunfictbso  8276  infmap2  8379  cofsmo  8430  cfsmolem  8431  coftr  8434  fin23lem11  8478  fincssdom  8484  fin23lem26  8486  isf32lem9  8522  ac6num  8640  gchdomtri  8788  gchpwdom  8829  winainflem  8852  tskuni  8942  gruima  8961  gruf  8970  grudomon  8976  elnpi  9149  distrlem4pr  9187  prlem934  9194  addcan  9545  addcan2  9546  ltmul1a  10170  ledivmulOLD  10198  ledivmul2OLD  10202  suprleub  10286  supmul1  10287  infmrgelb  10302  suprzcl  10713  uzsupss  10939  xleadd1a  11208  xlesubadd  11218  xmulasslem3  11241  xlemul2a  11244  xadddilem  11249  xadddi2  11252  ixxun  11308  icoshftf1o  11400  snunioc  11405  lincmb01cmp  11420  iccf1o  11421  fzofzim  11585  ltexp2a  11907  leexp2  11910  ltexp2r  11912  exple1  11915  expnlbnd2  11987  ccatass  12278  swrdswrdlem  12345  ccatopth  12356  cshco  12456  repsco  12459  s2f1o  12518  limsupgre  12951  addcn2  13063  mulcn2  13065  dvdsadd2b  13567  dvdsmod  13582  oexpneg  13587  gcdass  13721  rplpwr  13732  rppwr  13733  coprmdvds2  13781  rpmulgcd2  13783  qredeq  13784  rpexp  13798  rpdvds  13802  prmdiveq  13853  odzdvds  13859  modprmn0modprm0  13867  coprimeprodsq2  13869  pythagtriplem3  13877  pcdvdsb  13927  pcgcd1  13935  qexpz  13955  pockthg  13959  vdwnnlem1  14048  0ram  14073  ramz2  14077  lubss  15283  lubun  15285  clatleglb  15288  clatglbss  15289  mrelatglb  15346  issubmnd  15441  ress0g  15442  gsumccat  15510  frmdss2  15532  mulgneg  15636  mulgdirlem  15642  submmulg  15653  subgmulg  15686  nmzsubg  15713  ghmmulg  15750  gsmsymgreqlem1  15926  pmtrfb  15962  psgnunilem4  15994  odmodnn0  16034  odnncl  16039  odmod  16040  odmulgid  16046  odmulgeq  16049  odf1o1  16062  odf1o2  16063  odngen  16067  gexdvdsi  16073  pgpfi1  16085  odcau  16094  subgslw  16106  fislw  16115  lsmssv  16133  lsmless1x  16134  lsmless2x  16135  lsmsubm  16143  lsmmod  16163  lsmmod2  16164  efgred  16236  cntzcmn  16315  ghmplusg  16319  odadd1  16321  odadd2  16322  odadd  16323  lsmcomx  16329  gsumconst  16417  rng1eq0  16672  mulgass2  16680  isabvd  16883  lssintcl  17022  0lmhm  17098  lmhmvsca  17103  reslmhm2b  17112  pwssplit1  17117  pwssplit3  17119  lspfixed  17186  lspsnat  17203  lidldvgen  17314  issubassa  17372  evlsval2  17581  psrplusgpropd  17665  coe1subfv  17695  coe1mul2  17698  xrsdsreclblem  17834  regsumsupp  18027  obselocv  18128  uvcresum  18193  frlmsslsp  18198  frlmsslspOLD  18199  frlmup4  18204  lindff1  18224  f1lindf  18226  lsslindf  18234  islindf4  18242  lbslcic  18245  mhmvlin  18272  mamutpos  18318  mavmulsolcl  18337  marrepcl  18350  mdetunilem1  18393  mdetunilem3  18395  mdetunilem7  18399  mdetunilem9  18401  mdetmul  18404  slesolinvbi  18462  riinopn  18496  neiint  18683  topssnei  18703  restntr  18761  iscnp4  18842  cnconst2  18862  cnrest2  18865  cnprest2  18869  cnpdis  18872  cnt0  18925  cnt1  18929  cnhaus  18933  ordthauslem  18962  cncmp  18970  fiuncmp  18982  sscmp  18983  hauscmp  18985  cnconn  19001  uncon  19008  nlly2i  19055  llynlly  19056  nllyidm  19068  ptrescn  19187  xkococnlem  19207  qtoptop2  19247  qtopss  19263  kqfvima  19278  r0cld  19286  ordthmeolem  19349  fbssint  19386  fmf  19493  fmss  19494  elfm  19495  rnelfmlem  19500  rnelfm  19501  fmco  19509  flimss2  19520  flimss1  19521  flimrest  19531  flftg  19544  cnpflf2  19548  cnpflf  19549  flfcnp  19552  supnfcls  19568  fclsss1  19570  fclsss2  19571  fcfnei  19583  fcfelbas  19584  cnpfcfi  19588  subgntr  19652  opnsubg  19653  cldsubg  19656  ghmcnp  19660  utop2nei  19800  neipcfilu  19846  bldisj  19948  blgt0  19949  bl2in  19950  blss2ps  19953  blss2  19954  blssps  19974  blss  19975  xmetresbl  19987  lpbl  20053  blcld  20055  stdbdbl  20067  metcnp3  20090  metcnp2  20092  txmetcnp  20097  blval2  20125  nmoix  20283  nmoeq0  20290  icoopnst  20486  iocopnst  20487  xrhmeo  20493  nmhmcn  20650  cphsqrcl2  20680  cphsqrcl3  20681  cfil3i  20755  caublcls  20794  bcthlem5  20814  cmetcusp1OLD  20838  cmetcusp1  20839  rrxcph  20871  pjth  20901  ovoliunlem2  20961  volun  21001  volsup2  21060  mbfimaopn2  21110  iblconst  21270  itgconst  21271  dvcnp2  21369  dvcn  21370  deg1mul3le  21563  deg1tmle  21564  dvdsq1p  21607  ig1peu  21618  ig1pdvds  21623  coeid3  21683  dgrmulc  21713  efcvx  21889  tanord  21969  logdivlti  22044  logccv  22083  recxpcl  22095  cxpeq  22170  ang180  22185  isosctrlem2  22192  cxp2lim  22345  amgm  22359  muval1  22446  dvdssqf  22451  mumullem2  22493  mumul  22494  bcmono  22591  lgsfcl2  22616  lgsdilem  22636  lgsdirprm  22643  lgsdir  22644  lgsdi  22646  lgsne0  22647  brbtwn2  23102  colinearalglem1  23103  colinearalg  23107  axcgrtr  23112  axsegconlem8  23121  axsegconlem9  23122  axsegconlem10  23123  axcontlem8  23168  axcontlem10  23170  2pthon  23452  gxcom  23707  gxnn0add  23712  zerdivemp1  23872  nvmul0or  23983  ipval2lem2  24050  ipval2lem5  24056  lnomul  24111  shless  24713  shlej1  24714  pjspansn  24931  hoadddi  25158  kbmul  25310  homco2  25332  kbass2  25472  eliccelico  26018  elicoelioo  26019  iocinioc2  26020  iocinif  26022  xrge0adddir  26106  xrge0npcan  26108  archiabl  26166  ress1r  26208  rhmdvdsr  26237  pstmfval  26275  fmcncfil  26313  zrhnm  26350  qqhnm  26371  measvunilem  26578  volfiniune  26598  dya2iocnrect  26648  sibfinima  26677  probun  26754  probinc  26756  cndprob01  26770  signswmnd  26910  pconpi1  27078  cvmsss2  27115  ntrivcvgmul  27368  binomrisefac  27496  dvdspw  27507  br6  27518  br4  27519  frrlem4  27722  cgrcomim  27971  cgrtriv  27984  cgrextend  27990  segconeq  27992  btwntriv2  27994  btwnintr  28001  btwnexch3  28002  btwnouttr2  28004  trisegint  28010  cgrsub  28027  cgrxfr  28037  btwnxfr  28038  lineext  28058  btwnconn1lem13  28081  btwnconn1lem14  28082  btwnconn3  28085  segcon2  28087  brsegle  28090  brsegle2  28091  segletr  28096  segleantisym  28097  seglelin  28098  outsideofeu  28113  lineunray  28129  lineelsb2  28130  areacirc  28442  ivthALT  28483  finlocfin  28524  cocanfo  28564  upixp  28576  ismtyima  28655  rrndstprj2  28683  zerdivemp1x  28714  mzprename  29039  eldioph2lem1  29051  lzunuz  29059  rencldnfi  29113  pellexlem2  29124  infmrgelbi  29172  pellfundglb  29179  pellfund14gap  29181  qirropth  29202  rmxycomplete  29211  congadd  29262  acongeq  29279  jm2.19  29295  jm2.23  29298  jm2.20nn  29299  jm2.27  29310  jm3.1  29322  aomclem6  29365  lnmepi  29391  lmhmfgsplit  29392  lmhmlnmsplit  29393  pwssplit4  29395  hbtlem2  29433  hbtlem5  29437  dgraa0p  29459  hashgcdlem  29518  proot1hash  29521  iocunico  29539  stoweidlem19  29767  stoweidlem20  29768  stoweidlem22  29770  stoweidlem28  29776  stoweidlem34  29782  stoweidlem44  29792  stoweidlem60  29808  wallispilem3  29815  fzoopth  30166  clwwlkfo  30412  clwwlkext2edg  30417  erclwwlksym  30437  erclwwlknsym  30453  clwlkfoclwwlk  30471  clwlkf1clwwlklem  30475  numclwwlk2lem1  30648  numclwwlk5  30658  frgraregord13  30665  ofaddmndmap  30686  pmatcollpw1  30819  mdetdiag  30825  lincdifsn  30847  lincellss  30849  lincresunit3lem3  30897  islindeps2  30906  lindssnlvec  30909  bnj517  31765  bnj594  31792  lsatfixedN  32494  lssat  32501  eqlkr  32584  eqlkr2  32585  lkrlsp  32587  lshpkrlem4  32598  opposet  32666  cvrcon3b  32762  cvrcmp  32768  atlen0  32795  atnle  32802  atlatmstc  32804  cvlatexch3  32823  cvlsupr2  32828  hlsupr2  32871  hlrelat2  32887  cvrexchlem  32903  lnnat  32911  atcvrj2b  32916  atle  32920  atexchcvrN  32924  atbtwn  32930  athgt  32940  3dimlem3  32945  3dim1  32951  1cvratlt  32958  1cvrjat  32959  ps-1  32961  ps-2  32962  3atlem3  32969  3atlem5  32971  3atlem7  32973  llni  32992  llni2  32996  atcvrlln2  33003  llnexatN  33005  llncmp  33006  2llnmat  33008  2at0mat0  33009  lplni  33016  lplnnle2at  33025  2atnelpln  33028  lplnllnneN  33040  llncvrlpln2  33041  2lplnmN  33043  2llnmj  33044  lplncmp  33046  lplnexatN  33047  lplnexllnN  33048  2llnm3N  33053  lvoli  33059  lvoli3  33061  islvol2aN  33076  4atlem0a  33077  4atlem3  33080  4atlem3a  33081  4atlem4a  33083  4atlem4b  33084  4atlem4c  33085  4atlem4d  33086  4atlem10b  33089  4atlem11  33093  4atlem12  33096  lplncvrlvol2  33099  lvolcmp  33101  2lplnmj  33106  islinei  33224  pmapglbx  33253  linepmap  33259  lneq2at  33262  lnjatN  33264  lncvrat  33266  lncmp  33267  2llnma3r  33272  elpaddatriN  33287  elpaddat  33288  paddcom  33297  paddss1  33301  paddss2  33302  paddss12  33303  paddasslem6  33309  paddasslem7  33310  paddasslem8  33311  paddasslem9  33312  paddasslem15  33318  pmodlem2  33331  pmodl42N  33335  pmapjoin  33336  llnmod1i2  33344  2polcon4bN  33402  polcon2bN  33404  poml4N  33437  poml6N  33439  osumcllem1N  33440  osumcllem2N  33441  osumcllem11N  33450  osumclN  33451  pmapojoinN  33452  pexmidlem2N  33455  pexmidlem3N  33456  pexmidlem4N  33457  pexmidlem6N  33459  pexmidlem7N  33460  pl42lem2N  33464  pl42lem3N  33465  pl42lem4N  33466  pl42N  33467  lhpexle2lem  33493  lhpexle3lem  33495  lhpexle3  33496  lhpmcvr3  33509  lhp2at0nle  33519  lhprelat3N  33524  4atex  33560  4atex2  33561  lauteq  33579  lautco  33581  ltrncoidN  33612  ltrneq2  33632  ltrnnidn  33658  ltrnideq  33659  trlnid  33663  ltrnatlw  33667  trlnle  33670  trlval3  33671  trlval4  33672  cdlemc  33681  cdlemd5  33686  cdlemd9  33690  ltrneq3  33692  cdleme0moN  33709  cdleme20  33808  cdleme21j  33820  cdleme21  33821  cdleme27cl  33850  cdlemefrs29bpre0  33880  cdlemefs27cl  33897  cdlemefs32sn1aw  33898  cdleme43fsv1snlem  33904  cdleme32d  33928  cdleme32f  33930  cdleme32le  33931  cdleme35h2  33941  cdleme38n  33948  cdleme40m  33951  cdleme41snaw  33960  cdleme42ke  33969  cdleme17d3  33980  cdleme48fvg  33984  cdlemeg46fvcl  33990  cdlemeg46fgN  34018  cdleme48gfv1  34020  cdleme48fgv  34022  cdleme50trn3  34037  trlord  34053  ltrniotavalbN  34068  cdlemb3  34090  cdlemg6c  34104  cdlemg6  34107  cdlemg7N  34110  cdlemg8c  34113  cdlemg8  34115  cdlemg11a  34121  cdlemg11b  34126  cdlemg12e  34131  cdlemg15a  34139  cdlemg15  34140  cdlemg16  34141  cdlemg16z  34143  cdlemg16zz  34144  cdlemg17dN  34147  cdlemg18a  34162  cdlemg20  34169  cdlemg22  34171  cdlemg24  34172  cdlemg37  34173  cdlemg31d  34184  cdlemg29  34189  cdlemg33b  34191  cdlemg33  34195  cdlemg38  34199  cdlemg39  34200  cdlemg40  34201  trlco  34211  trlcone  34212  cdlemg42  34213  cdlemg44b  34216  ltrncom  34222  trljco  34224  tendococl  34256  tendoplcl  34265  tendoplcom  34266  cdlemj2  34306  cdlemj3  34307  tendoid0  34309  tendoconid  34313  tendotr  34314  cdlemk25-3  34388  cdlemk26b-3  34389  cdlemk34  34394  cdlemk36  34397  cdlemk38  34399  cdlemkid4  34418  cdlemk35s-id  34422  cdlemk39s-id  34424  cdlemk19x  34427  cdlemk53  34441  cdlemk55  34445  cdlemk55u  34450  cdlemk39u  34452  cdlemk19u  34454  cdlemk56  34455  tendoex  34459  cdleml3N  34462  cdleml5N  34464  tendospcanN  34508  cdlemm10N  34603  cdlemn11pre  34695  dihord2pre  34710  dihvalcqpre  34720  dihopelvalcpre  34733  dihord6apre  34741  dihord5b  34744  dihord5apre  34747  dihord  34749  dihmeetlem1N  34775  dihglblem5apreN  34776  dihglblem3N  34780  dihmeetlem2N  34784  dihglbcpreN  34785  dihmeetbN  34788  dihmeetlem4preN  34791  dihmeetlem5  34793  dihmeetlem7N  34795  dihmeetlem10N  34801  dihmeetlem11N  34802  dihmeetlem12N  34803  dihmeetlem13N  34804  dihmeetlem15N  34806  dihmeetlem16N  34807  dihmeetlem17N  34808  dihmeetlem18N  34809  dihmeetlem19N  34810  dihmeetALTN  34812  dih1dimatlem0  34813  dihlspsnssN  34817  dihlspsnat  34818  mapdh8ad  35264  hdmap14lem14  35369  hgmapvvlem3  35413