Theorem syl 10

Description: An inference version of the transitive laws for implication imim2 14 and imim1 15, which Russell and Whitehead call "the principle of the syllogism...because...the syllogism in Barbara is derived from them" (quote after Theorem *2.06 of [WhiteheadRussell] p. 101). Some authors call this law a "hypothetical syllogism."

(A bit of trivia: this is the most commonly referenced assertion in our database. In second place is ax-mp 7, followed by visset 1816, bitr 173, imp 350, and ex 373. The Metamath program command 'show usage' shows the number of references.)

Hypotheses

Ref	Expression
syl.1	|- (ph -> ps)
syl.2	|- (ps -> ch)

Assertion

Ref	Expression
syl	|- (ph -> ch)

Proof of Theorem syl

Step	Hyp	Ref	Expression
1		syl.1	. 2 |- (ph -> ps)
2		syl.2	. . . 4 |- (ps -> ch)
3	2	a1i 8	. . 3 |- (ph -> (ps -> ch))
4	3	a2i 9	. 2 |- ((ph -> ps) -> (ph -> ch))
5	1, 4	ax-mp 7	1 |- (ph -> ch)

Syntax hints:   -> wi 3

This theorem is referenced by:  com12 11  a1d 12  a2d 13  imim12i 18  3syl 20  syl5 21  syl6 22  imim1d 28  com23 32  sylcom 51  sylc 68  pm2.86d 71  a3d 75  peirce 82  nega 84  pm2.01 88  pm2.01d 89  con2d 91  con1d 93  con3d 95  con1i 96  con2i 97  con3i 98  nsyl 116  nsyl2 118  nsyl3 119  nsyl4 120  bi1 148  bi2 149  biimpd 153  biimprd 154  bitr 173  sylib 198  sylbi 199  sylibr 200  sylbir 201  orcd 272  olcd 273  orcs 274  olcs 275  ancld 298  ancrd 299  pm3.26d 321  pm3.27d 325  anim12i 333  jao 340  sylan 450  condan 480  pm4.72 643  pm5.75 751  elimh 766  dedt 767  oplem1 774  3simp1d 796  3simp2d 797  3simp3d 798  3adant1 799  3adant2 800  3adant3 801  syl3anc 860  syl3an 870  meredith 926  ax4 974  ax5 978  a4s 986  a7s 993  19.20 996  19.20ii 997  19.20d 998  19.21ai 1000  hbal 1007  ax46to4 1020  ax46to6 1021  ax67 1022  ax67to7 1024  ax467to4 1026  ax467to6 1027  ax467to7 1028  19.18 1052  19.21bi 1062  19.22d 1064  19.23bi 1067  19.29r2 1075  19.29x 1076  19.25 1086  19.33b 1094  albid 1106  exbid 1107  hbnd 1111  ax9o 1124  equid 1128  equcoms 1132  ax10o 1141  ax10 1143  alequcoms 1145  hbae 1147  hbaes 1148  hbnaes 1150  equs4 1152  equsal 1153  a4im 1161  stdpc4 1187  sbf 1188  sbied 1197  sb4a 1201  equs45f 1202  sb6f 1203  sb4e 1205  hbsb2a 1206  hbsb2e 1207  hbsb3 1208  ax16 1211  ax11v2 1217  sbequi 1230  sbbid 1248  sbco3 1259  ax16i 1272  a16g 1278  sbal2 1360  ax11eq 1365  ax11el 1366  ax11indalem 1370  ax11inda2ALT 1371  ax11inda 1373  a12lem1 1378  a12study 1380  mo 1395  mo2 1402  exmoeu 1415  euor2 1440  moexex 1441  2euex 1444  2eu2ex 1446  2mo 1450  2eu1 1452  2eu5 1456  exists2 1461  bm1.1 1465  hbabd 1471  eqeq1d 1486  eqeq2d 1489  eleq1d 1543  eleq2d 1544  neeq1d 1597  neeq2d 1598  r19.20sii 1710  r19.22d 1738  r19.12 1743  raleq1d 1792  rexeq1d 1793  cgsexg 1834  cgsex2g 1835  cgsex4g 1836  ceqsex 1837  vtoclgf 1849  vtocleg 1858  vtoclegft 1859  cla4gf 1863  rcla4edv 1882  rcla42ev 1884  hbeqd 1916  hbeld 1917  dedhb 1918  moeq3 1924  sbcco2 1956  sbcieg 1964  elrabsf 1966  elabsg 1968  sbcel1gv 1983  sbcel2gv 1984  hbsbc1gd 1986  hbsbcgd 1987  sbcralt 1993  sbcralgf 1995  sbcralg 1997  sbcrexg 1998  sbcabel 1999  csbeq1d 2007  sbcel12g 2014  sbceqdig 2015  csbvarg 2024  hbcsb1g 2027  hbcsbg 2029  csbnestg 2039  sbcnestg 2041  csbidmg 2042  sbcco3g 2044  csbabg 2046  sseld 2070  sseq1d 2091  sseq2d 2092  psseq1d 2143  psseq2d 2144  pssssd 2147  difeq1d 2161  difeq2d 2162  uneq1d 2186  uneq2d 2187  ineq1d 2219  ineq2d 2220  uneqin 2259  reuss2 2278  ssdisj 2322  disjssun 2330  ifeq1d 2373  ifeq2d 2374  ifbid 2376  elimif 2378  ifboth 2379  ifswap 2386  dedth 2387  dedth2v 2388  dedth3v 2389  dedth4v 2390  elimhyp 2394  elimhyp2v 2395  elimhyp3v 2396  elimhyp4v 2397  elimdhyp 2399  keephyp2v 2401  keephyp3v 2402  sneqd 2423  elpr2 2429  ifpr 2431  snsspr 2474  opeq1 2491  opeq2 2492  opeq1d 2497  opeq2d 2498  hbopd 2501  opprc1 2502  opprc2 2503  unieqd 2516  unimax 2536  inteqd 2542  elinti 2546  intmin3 2562  intmin4 2563  intab 2564  iuneq2dv 2586  iineq2dv 2587  iinss 2604  iununi 2621  breq1d 2634  breq2d 2635  hbbrd 2664  sbcbrg 2667  sbcbr12g 2668  csbopabg 2683  axrep1 2699  zfrepclf 2704  nalset 2717  elssabg 2731  intex 2734  class2seteq 2740  abssexg 2753  rext 2760  pwel 2765  euabex 2773  exss 2775  dtru 2778  opth1 2792  opth 2793  copsex2g 2799  oteqex 2805  opth2 2806  moop2 2807  mosubopt 2810  opthwiener 2813  pwssun 2833  difex2 2883  opeluu 2885  euuni 2887  reuuniss 2895  reuuniss2 2897  ralxfr 2905  reuxfr2 2909  reuxfr 2910  reuhyp 2911  reuunixfr 2912  eldifpw 2916  elpwun 2917  elpwunsn 2918  iunpw 2920  frirr 2930  fr2nr 2931  fr3nr 2932  wereucl 2952  ordfr 2969  ordirr 2972  ordn2lp 2974  ordelord 2976  tz7.7 2979  ordtri3or 2985  onsst 2998  ssorduni 2999  ssonunit 3000  orduni 3003  ordtr1 3007  ontr1 3009  ordunidif 3011  onssmin 3014  onminsb 3015  onminesb 3016  bm2.5ii 3025  onminex 3026  on0eln0 3030  limuni2 3036  0ellim 3037  ordsssuc2 3065  suceloni 3068  ordnbtwn 3069  onnbtwn 3070  ordsuc 3071  onpwsuc 3073  ordssun 3085  ordequn 3086  ordsucun 3088  ordsucuni 3092  unon 3094  ordunisuc 3095  onsucuni2 3097  suc11 3099  onuninsuc 3114  ordunisuc2 3121  dflim3 3124  nlimon 3128  limuni3 3129  dfom2 3139  nnord 3146  ordom 3147  nnlim 3150  peano5 3159  findes 3166  tfinds 3167  tfindsg2 3169  tfindes 3170  otelxp1 3212  vtoclr 3217  vtoclibr 3219  ralxp 3224  onxpdisj 3247  relssdv 3255  xpsspw 3263  xpexg 3265  relop 3281  ideqg 3282  opelxpex2 3285  coeq1d 3291  coeq2d 3292  dmeqd 3319  rneqd 3347  rnss 3348  dmrnssfld 3363  dmcoeq 3372  ssres2 3392  resiexg 3402  iss 3403  imaeq1d 3409  imaeq2d 3410  hbimad 3418  imaexg 3422  imasng 3430  iniseg 3436  imass1 3438  imass2 3439  asymref 3445  asymref2 3446  xpsndisj 3476  dmxpss 3479  rnxpss 3480  xp11 3482  cores2 3513  coexg 3530  funopg 3553  funssres 3558  fun2ssres 3559  funun 3560  fununi 3569  funcnvuni 3570  fun11uni 3571  funcnvres2 3576  funimaexg 3581  cofunexg 3586  cofunex2g 3587  fnrel 3592  fnco 3601  fnresdm 3602  2elresin 3604  fnssresb 3605  fnima 3610  fn0 3611  fnex 3613  opabex2g 3617  fnopabg 3621  feq1d 3630  ffun 3635  frel 3636  fdm 3637  fss 3641  fco 3642  fssxp 3643  funssxp 3644  ffdm 3645  fcoi1 3651  fcoi2 3652  f00 3663  fconst 3664  fconstg 3665  f1eq1 3666  fofun 3679  fornex 3685  fodmrnu 3686  foconst 3689  f1of 3695  f1ofn 3696  f1ofun 3697  f1orel 3698  f1o5 3703  f1f1orn 3705  f1oabexg 3706  f1ocnv 3707  f1orescnv 3710  f1imacnv 3711  f1ococnv2 3714  f1ococnv1 3715  f1dmex 3716  f1o00 3720  fveq1d 3732  fveq2d 3734  hbfvd 3736  hbfvd2 3737  tz6.12i 3747  elfvdm 3753  nfvres 3754  fnopabfv 3764  fnsnfv 3773  ssimaex 3774  funfv2 3777  fvopab4ndm 3790  fvopab2 3797  fvopab5 3799  fvreseq 3805  elrnopabg 3806  fvelrn 3818  dff4 3822  dff2 3823  dffo3 3825  dffo4 3826  dffo5 3827  exfo 3828  fopab2 3829  fopabco 3838  fopabcos 3839  fsn 3840  fsn2 3842  fnressn 3843  fressnfv 3844  fvconst 3845  fconst2g 3851  fconst3 3856  abrexex 3866  iunexg 3868  f1fv 3880  f1fveq 3882  f1ocnvfv1 3884  f1ocnvfv2 3885  f1ofveu 3888  f1ocnvfv3 3889  f1ocnvdm 3890  cbvfo 3891  isocnv 3902  isotr 3903  isotrALT 3904  isomin 3905  isoini 3906  isofrlem 3907  isofr 3908  isowe 3909  f1oweALT 3912  canth 3913  iunon 3915  tfrlem2 3918  tfrlem5 3921  tfrlem6 3922  tfrlem8 3924  tfrlem9 3925  tfrlem11 3927  tfrlem12 3928  tfrlem13 3929  tfr3 3932  tz7.44lem1 3933  tz7.44-2 3935  tz7.44-3 3936  dfrdg2 3939  rdglem2 3944  rdglim2 3955  frsuct 3959  tz7.48lem 3961  tz7.48-1 3962  tz7.48-2 3963  tz7.48-3 3964  tz7.49 3965  tz7.49c 3966  abianfplem 3967  abianfp 3968  opreq1d 3981  opreq2d 3982  opreqd 3983  hboprd 3988  oprprc1 3990  fnoprabg 4018  oprabex2g 4026  oprabval 4029  oprvalres 4039  oprssoprval 4040  oprvalconst2 4046  oprssdm 4048  ndmoprass 4054  ndmoprdistr 4055  ndmord 4056  ndmordi 4057  caoprmo 4076  2ndval2 4096  curry1 4104  1stcof 4107  eqop 4110  1st2nd 4114  1stdm 4115  2ndrn 4116  dfopab2 4119  dfoprab3 4120  dfoprab5 4121  oe0m1 4166  oa1suc 4170  oesuc 4172  oaordi 4186  oaord 4187  oacan 4188  oaword 4189  oawordri 4190  oawordeulem 4194  oalimcl 4200  oaass 4201  oarec 4202  omordi 4203  omcan 4206  omword 4207  omwordi 4208  omword1 4210  om00 4212  om00el 4213  omlimcl 4215  odi 4216  omass 4217  oneo 4218  oen0 4219  oeordi 4220  oecan 4222  oeword 4223  oewordi 4224  oewordri 4225  oeworde 4226  oelim2 4228  nna0 4229  nnm0 4230  nna0r 4233  nnm0r 4234  nnecl 4237  nnarcl 4238  nnacom 4239  nnmsucr 4246  oaabslem 4257  oaabs 4258  nneob 4261  omsmo 4263  erthdm 4289  ecopqsi 4299  ectocl 4308  ecoptocl 4309  brecop 4312  brecop2 4313  ecopoprdm 4315  ecopoprsym 4316  eceqopreq 4319  th3qlem1 4320  th3qlem2 4321  th3q 4323  oprec 4324  ecoprcom 4325  ecoprass 4326  ecoprdi 4327  pmex 4333  mapex 4334  elmapg 4339  mapval2 4341  map0b 4349  mapsn 4351  mapss 4352  uniixp 4363  ixpexg 4364  ixp0 4367  breng 4381  brdomg 4382  enrefg 4396  domrefg 4399  en2d 4406  idssen 4412  ener 4416  ensymg 4417  domtr 4421  f1imaen 4428  en0 4429  en1 4432  2dom 4433  fundmen 4434  en2sn 4437  snfi 4438  snfiOLD 4439  unen 4440  xpsnen 4441  xpsneng 4442  undom 4444  xpcomen 4445  xpdom2 4448  xpdom1 4449  pw2en 4452  sbthlem2 4454  sbthlem4 4456  sbthlem8 4460  sbthlem10 4462  ensdomtr 4477  sdomtr 4480  domsdomtr 4482  enen1 4483  domen1 4485  sdomen1 4487  fodomr 4489  mapenlem2 4496  mapen 4497  mapdom1 4498  mapdom2lem 4499  mapdom2 4500  mapxpen 4501  xpmapenlem3 4504  xpmapenlem5 4506  mapunen 4508  ssenen 4510  phplem1 4514  phplem2 4515  phplem3 4516  phplem4 4517  php 4519  php2 4520  php3 4521  php3OLD 4522  php5 4524  onomeneq 4525  ominf 4536  ominfOLD 4537  isfinite1 4539  isfinite1OLD 4540  pssnn 4544  ssfi 4547  ssfiOLD 4548  domfiOLD 4550  unblem1 4551  unblem2 4552  unblem3 4553  unblem4 4554  unbnn 4555  unfilem1 4560  unfilem3 4562  unfi 4563  unfiOLD 4564  unfi2 4565  unfi2OLD 4566  unifiOLD 4570  unifi2OLD 4571  fiint 4572  fiintOLD 4573  fodomfi 4575  fodomfiOLD 4576  pwfilem 4577  pwfilemOLD 4578  pwfi 4579  pwfiOLD 4580  pm54.43 4581  supcl 4588  supmax 4598  supsnALT 4601  opthreg 4613  inf3lemd 4621  inf3lem5 4626  inf3lem7 4628  infeq5 4630  isfinite 4643  isfiniteOLD 4644  nnsdom 4645  infensuc 4648  noinfep 4650  trcl 4655  zfregs 4657  setind 4658  r1tr 4664  r1ord 4665  r1ord3 4667  r1val1 4668  tz9.12lem3 4671  tz9.12 4672  tz9.13 4673  rankwflem 4675  rankon 4681  rankr1 4684  r1val3 4689  rankval3 4691  bndrank 4692  ranklim 4695  r1pw 4696  r1pwcl 4697  rankuni2 4700  rankun 4701  rankonid 4705  rankr1id 4707  rankuni 4708  rankval4 4712  rankbnd2 4714  rankelun 4717  rankxplim 4722  rankxplim2 4723  rankxplim3 4724  rankxpsuc 4725  scottex 4726  scott0 4727  bnd2 4734  aceq3lem 4742  aceq3 4743  aceq5lem3 4747  aceq5lem4 4748  aceq5lem5 4749  aceq6a 4751  aceq6b 4752  ac7g 4759  ac6lem 4764  ac6 4765  ac6s 4766  ac6s2 4768  ac6s3 4769  ac6s5 4772  kmlem1 4775  kmlem8 4782  kmlem11 4785  kmlem13 4787  numth2 4795  numthcor 4796  weth 4797  zorn2lem2 4799  zorn2lem3 4800  zorn2lem4 4801  zorn2lem5 4802  zorn2lem6 4803  zorn2 4806  zorn 4807  fodom 4808  fodomb 4810  brdom3 4811  brdom4 4813  brdom7disj 4814  brdom6disj 4815  imadomg 4816  unidom 4818  uniimadom 4820  oncardval 4829  oncardon 4830  oncardid 4831  cardnn 4834  cardom 4835  oncard 4839  carden 4841  carddomi 4845  entri3 4851  unxpdom2 4856  sucxpdom 4857  cardlim 4862  cardsdomel 4863  iscard 4864  ondomon 4867  ondomcard 4868  carduni 4869  cardiun 4870  cardmin 4871  alephordi 4885  alephord 4886  alephle 4895  cardaleph 4896  carduniima 4901  cardinfima 4902  alephfplem3 4909  alephfp 4911  alephval2 4913  cfub 4920  cflim 4921  cardcf 4923  cflecard 4924  cfle 4925  cfeq0 4926  cfsuc 4927  cdafi 4948  axrepndlem1 4956  axrepndlem2 4957  axrepnd 4958  axunndlem1 4959  axunnd 4960  axpowndlem2 4962  axpowndlem3 4963  axpowndlem4 4964  axpownd 4965  axregndlem2 4967  axinfndlem1 4969  axinfnd 4970  axacndlem1 4971  axacndlem2 4972  axacndlem3 4973  axacndlem4 4974  axacndlem5 4975  axacnd 4976  zfcndinf 4982  elni2 5017  pion 5019  piord 5020  addpiord 5024  mulpiord 5025  mulclpi 5033  addnidpi 5040  indpi 5046  addcmpblnq 5064  mulcmpblnq 5065  ordpipq 5068  distrpqlem 5078  distrpq 5079  recmulpq 5082  recclpq 5084  recrecpq 5085  dmrecpq 5086  ltsopq 5087  ltapq 5088  ltmpq 5089  ltexpq 5092  halfpq 5094  ltrpq 5097  elnp 5104  genpnnp 5120  genpnmax 5122  mulclprlem 5133  distrlem4pr 5142  1idpr 5145  prlem934a 5149  prlem934b 5150  prlem934 5151  ltexprlem2 5155  ltexprlem4 5157  ltexprlem6 5159  ltexprlem7 5160  ltaprlem 5162  ltapr 5163  reclem1pr 5168  reclem2pr 5169  reclem3pr 5170  reclem4pr 5171  recexpr 5172  suplem2pr 5174  addcmpblnr 5193  mulcmpblnr 5195  ltsrpr 5198  ltsosr 5215  ltasr 5221  recexsrlem 5224  addgt0sr 5225  sqgt0sr 5227  ssgt0sr 5229  mappsrpr 5230  suppsr2 5235  suppsr3 5236  supsrlem1 5237  supsrlem2 5238  mulresr 5269  axaddopr 5277  axmulopr 5278  axmulass 5290  axdistr 5291  recnd 5327  cnegextlem2 5358  cnegextlem3 5359  cnegext 5360  negeqd 5373  hbnegd 5375  renegcl 5428  muladd11t 5434  1re 5447  pnpcant 5490  ltxrltt 5512  xrlenltt 5513  axmulgt0 5518  ltpnft 5554  mnfltt 5555  xrltnsymt 5562  xrlttrt 5565  addge0 5611  mulge0 5619  msqge0 5626  ne0gt0t 5631  ltaddpost 5663  ltnegcon1t 5668  lenegcon1t 5670  lenegcon2t 5671  addge01t 5684  suble0t 5687  recextlem1 5694  recext 5696  muleqaddt 5712  divasst 5748  div0t 5768  divcan5t 5783  divadddivt 5786  divdivdivt 5787  conjmult 5799  redivcl 5800  negeq0t 5808  ltm1t 5817  ltmuldiv 5827  mulgt1t 5847  ltmulgt11t 5848  lemulge11t 5850  lediv1tOLD 5854  lerec 5882  recgt1it 5902  recp1lt1 5903  recrecltt 5904  ledivp1 5908  ltdivp1 5909  posex 5910  nn1suc 5941  nnge1t 5945  nnle1eq1t 5947  nnrecgt0t 5955  nnleltp1t 5956  nnsub 5958  nnaddm1clt 5960  nndivt 5961  nndivtrt 5962  halfaddsubcl 6042  lt2halvest 6044  avglet 6046  lbreu 6047  lble 6049  lbinfm 6050  sup2 6053  infm3lem 6055  suprcl 6057  suprub 6058  suprlub 6059  suprnub 6060  infmrcl 6071  nnreclt 6074  xrsupsslem 6078  xrinfmsslem 6079  xrsupss 6080  xrinfmss 6081  xrub 6082  supxrre 6085  supxrcl 6086  supxrun 6087  infmxrcl 6088  supxrmnf 6089  supxrbnd 6093  supxrgtmnf 6094  supxrbnd1 6097  supxrbnd2 6098  xrsup0 6099  supxrub 6100  supxrleub 6101  nn0le0eq0t 6121  nn0addclt 6122  nn0mulcl 6124  nnnn0addclt 6127  nn0ltp1let 6129  nn0ltlem1t 6131  nnnegz 6140  elnnz 6147  elnn0z 6149  elznn0 6151  elznn 6152  elnnz1 6157  znnnlt1t 6158  nn0subt 6163  nn0negz 6166  peano2zd 6169  elnn0nn 6173  zltp1let 6183  zlem1ltt 6185  zltlem1t 6186  zextlet 6191  recnzt 6193  btwnnzt 6194  gtndivt 6195  nneo 6199  zeot 6201  zneo 6202  dfuz 6204  uzind 6207  uzind2 6208  uzindOLD 6210  uzwo4OLD 6212  uzwo5OLD 6213  nn0ind-raph 6216  btwnz 6217  uzwo3lem2 6219  zmax 6222  zbtwnre 6223  rebtwnz 6224  flclt 6228  flreclt 6229  flleltt 6230  flget 6235  flidt 6237  flidmt 6238  flval3t 6241  fladdzt 6246  flhalft 6248  ceiget 6250  ceim1lt 6251  quoremz 6253  intfrac 6254  intfracq 6255  fldivt 6256  nnrecretOLD 6278  qbtwnre 6279  qbtwnxr 6280  monoord 6295  om2uzlt2 6300  om2uzran 6301  uzrdgsuc 6305  seq1lem2 6311  seq1val 6313  seq1suclem 6317  seq1m1 6320  seq1rn2 6322  seq1res 6328  ser1recl 6332  ser1p1 6337  ser1mono 6338  ser1add2 6339  ser1add 6340  shftfn 6344  shftf 6352  2shft 6353  seq1shftid 6357  ioo0t 6369  eliooret 6387  eliooxrt 6388  eliooordt 6389  ioossicc 6398  iccnegt 6408  icoshftf1oi 6410  icoshftf1olem 6411  uzidt 6428  uzssz 6431  uzss 6432  eluzp1m1t 6434  eluzaddi 6437  eluzsubi 6438  peano2uzr 6449  uzaddclt 6450  uzind4 6451  uzind4s 6453  uzind4s2 6454  uzwo 6456  uzwoOLD 6457  elfzlem 6474  elfzel1 6482  elfzelz 6483  elfzle1 6484  elfzle2 6485  elfzuz2t 6487  eluzfz1t 6488  elfz3t 6492  elfz1eqt 6493  fznt 6494  fzoptht 6503  fzssp1t 6507  fzp1sst 6508  elfzp1 6511  fznn0t 6517  fzrevralt 6520  fzshftralt 6523  fsequb 6524  fsequb2 6525  limsupvalt 6530  seq0fval 6536  seqzfval 6538  seqzfval2 6539  seqzfn 6540  seqzvalt 6541  seq1seqz 6542  seq1seq02t 6544  seqz1 6548  seqzp1 6549  seqzm1 6550  seq0p1 6552  seqzval2t 6554  seqzfveq 6555  seqzeq 6556  seqzrn 6558  seqzcl 6559  seqzres 6561  seqzres2 6562  ser0cl1 6565  ser0p1 6568  expvalt 6571  expnnvalt 6573  exp1t 6574  expcllem 6576  expm1t 6584  expgt0t 6590  expge0t 6592  expgt1t 6593  expge1t 6594  mulexpt 6595  recexpt 6596  expaddt 6597  expmult 6598  expordit 6601  expword2it 6606  expubndt 6609  sqnegt 6611  sqgt0t 6623  sqlecant 6642  subsq2t 6644  bernneq 6653  bernneq2 6654  expnbndt 6655  discrlem2 6658  discrlem3 6659  nnesq 6663  nn0opthlem2 6666  sqrval 6672  sqr0 6673  sqrlem6 6679  sqrlem12 6685  sqrlem13 6686  sqrlem17 6690  sqrlem18 6691  sqrge0 6703  sqsqr 6722  sqr2irr 6730  crrecz 6742  rimul 6745  reclt 6758  imclt 6759  replimt 6762  crret 6770  crimt 6771  imret 6774  reim0t 6775  reim0bt 6776  rerebt 6777  reret 6799  cjexpt 6817  recjt 6818  imcjt 6819  cjreimt 6828  cjreim2t 6829  cj11t 6830  absnegt 6832  abscjt 6834  sqabsaddt 6848  sqabssubt 6849  absreimsqt 6856  absreimt 6857  absdivz 6859  absnidt 6863  leabst 6864  absret 6866  absresqt 6867  absexpt 6868  absrelet 6869  absimlet 6870  leabs 6872  nn0absclt 6879  lenegsqt 6885  releabst 6886  cjdiv 6888  absmaxt 6897  abs3lem 6901  abs2dift 6902  abs2difabst 6903  abs1m 6904  seq1bnd 6910  seq1ublem 6911  seq1ub 6912  cau2 6913  cau3i 6914  cau5i 6917  cvg1i 6920  cvg2 6922  cvg3 6923  cvganz 6924  caubnd 6926  caure 6927  cauim 6928  ser1absdiflem 6929  facp1t 6936  facne0t 6941  facdivt 6942  facndivt 6943  facwordit 6944  faclbnd 6945  faclbnd2 6946  faclbnd3 6947  faclbnd4lem1 6948  faclbnd4lem3 6950  faclbnd4lem4 6951  faclbnd5 6953  faclbnd6 6954  facavgt 6955  bccmplt 6962  bcn0t 6963  bcnnt 6964  bcnp11t 6965  bcnp1nt 6966  bcpasc 6969  bccl2t 6971  bcclt 6972  permnnt 6973  sumeq2 6985  sumeq1d 6990  sumeq2d 6991  sumeq2dv 6992  2sumeq2dv 6994  sumeqfv 6997  fsumserz 6999  serzfsum 7004  fsum1 7005  fsump1 7006  fsump1s 7013  fsumcllem 7014  fsum1ps 7018  fsum1p 7019  fsumsplit 7020  fsum0split 7021  fsumadd 7022  fsum2 7023  fsum3 7024  fsum4 7025  fsumcom 7028  fsumrev 7029  fsumshft 7031  fsummulc1 7033  fsumconst 7038  fsum0 7039  fsumcmp 7040  fsumcmpndx2 7042  fsumabs 7043  fsumabs2mul 7044  ser1ser0 7048  serzref 7051  serz1p 7052  serz0 7053  serzcmp0 7055  serzsplit 7056  serzmulc 7058  serzrelem 7061  binomlem1 7066  binomlem2 7067  binomlem3 7068  binomlem4 7069  binomlem5 7070  binom1p 7073  bcxmas 7076  clm4 7080  clm4le 7081  clm0 7083  clm0nns 7085  clmi1 7086  clmi2 7087  clm0i 7089  climconst 7094  climconst3 7096  2climnn 7102  2climnn0 7103  climshft 7104  climshft2 7106  iserzshft2 7107  serzclim0 7109  climrecl 7110  climge0 7112  climabs0 7113  climaddlem3 7116  climmullem1 7120  climmullem2 7121  climmullem3 7122  climmullem4 7123  climmullem5 7124  climmullem8 7127  clim2serzt 7134  climcmplem 7137  climsqueeze 7140  climsqueeze2 7141  iserzcmp 7142 &