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 1788, 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 448  condan 477  pm4.72 639  pm5.75 746  elimh 761  dedt 762  oplem1 769  3simp1d 791  3simp2d 792  3simp3d 793  3adant1 794  3adant2 795  3adant3 796  syl3anc 855  syl3an 865  meredith 920  a4s 960  a7s 967  19.20 970  19.20ii 971  19.20d 972  19.21ai 974  hbal 981  ax46to4 992  ax46to6 993  ax67 994  ax67to7 996  ax467to4 998  ax467to6 999  ax467to7 1000  19.18 1026  19.21bi 1036  19.22d 1038  19.23bi 1041  19.29r2 1049  19.29x 1050  19.25 1060  19.33b 1068  albid 1080  exbid 1081  hbnd 1085  ax9 1110  equid 1113  equcoms 1117  alequcom 1125  alequcoms 1126  hbae 1128  hbaes 1129  hbnaes 1131  equs4 1133  equsal 1134  a4a 1142  hbequid 1152  stdpc4 1168  sbf 1169  sbied 1178  sb4a 1183  equs45f 1184  sb6f 1185  sb4e 1186  hbsb2a 1187  hbsb2e 1188  hbsb3 1189  ax16 1193  ax11v2 1199  sbequi 1212  sbbid 1230  sbco3 1241  a16g 1258  sbal2 1338  ax11eq 1340  ax11el 1341  ax11indalem 1345  ax11inda2ALT 1346  ax11inda 1348  a12lem1 1353  a12study 1355  mo 1370  mo2 1377  exmoeu 1390  euor2 1414  moexex 1415  2euex 1418  2eu2ex 1420  2mo 1424  2eu1 1426  2eu5 1430  exists2 1435  bm1.1 1439  hbabd 1445  eqeq1d 1459  eqeq2d 1462  eleq1d 1516  eleq2d 1517  neeq1d 1570  neeq2d 1571  r19.20sii 1683  r19.22d 1711  r19.12 1716  raleq1d 1765  rexeq1d 1766  cgsexg 1806  cgsex2g 1807  cgsex4g 1808  ceqsex 1809  vtoclgf 1821  vtocleg 1830  vtoclegft 1831  cla4gf 1835  rcla42ev 1853  hbeqd 1885  hbeld 1886  dedhb 1887  moeq3 1893  sbcco2 1924  sbcieg 1932  elrabsf 1934  elabsg 1936  sbcel1gv 1951  sbcel2gv 1952  hbsbc1gd 1954  hbsbcgd 1955  sbcralt 1961  sbcralgf 1963  sbcralg 1965  sbcrexg 1966  sbcabel 1967  csbeq1d 1975  sbcel12g 1982  sbceqdig 1983  csbvarg 1992  hbcsb1g 1995  hbcsbg 1997  csbnestg 2007  sbcnestg 2009  csbidmg 2010  sbcco3g 2012  csbabg 2014  sseld 2038  sseq1d 2059  sseq2d 2060  psseq1d 2111  psseq2d 2112  pssssd 2115  difeq1d 2129  difeq2d 2130  uneq1d 2154  uneq2d 2155  ineq1d 2187  ineq2d 2188  uneqin 2227  reuss2 2246  ssdisj 2289  disjssun 2297  ifeq1d 2340  ifeq2d 2341  ifbid 2343  elimif 2345  ifboth 2346  ifswap 2353  dedth 2354  dedth2v 2355  dedth3v 2356  dedth4v 2357  elimhyp 2361  elimhyp2v 2362  elimhyp3v 2363  elimhyp4v 2364  elimdhyp 2366  keephyp2v 2368  keephyp3v 2369  sneqd 2390  elpr2 2396  ifpr 2398  snsspr 2440  opeq1 2456  opeq2 2457  opeq1d 2462  opeq2d 2463  hbopd 2466  opprc1 2467  opprc2 2468  unieqd 2480  unimax 2500  inteqd 2506  elinti 2510  intmin3 2526  intmin4 2527  intab 2528  iuneq2dv 2550  iineq2dv 2551  iinss 2568  iununi 2584  breq1d 2597  breq2d 2598  hbbrd 2627  sbcbrg 2630  sbcbr12g 2631  csbopabg 2646  axrep1 2662  zfrepclf 2667  nalset 2680  elssabg 2694  intex 2697  class2seteq 2703  abssexg 2715  rext 2722  pwel 2727  euabex 2735  exss 2737  dtru 2740  opth 2754  copsex2g 2760  opth2 2765  moop2 2766  mosubopt 2767  opthwiener 2770  pwssun 2789  difex2 2840  opeluu 2842  euuni 2844  reuuniss 2852  reuuniss2 2854  ralxfr 2862  reuxfr2 2866  reuxfr 2867  reuhyp 2868  reuunixfr 2869  eldifpw 2873  elpwun 2874  elpwunsn 2875  iunpw 2877  frirr 2887  fr2nr 2888  fr3nr 2889  wereucl 2909  ordfr 2926  ordirr 2929  ordn2lp 2931  ordelord 2933  tz7.7 2936  ordtri3or 2942  onsst 2955  ssorduni 2956  ssonunit 2957  orduni 2960  ordtr1 2964  ontr1 2966  ordunidif 2968  onssmin 2971  onminsb 2972  onminesb 2973  bm2.5ii 2982  onminex 2983  on0eln0 2987  limuni2 2993  0ellim 2994  ordsssuc2 3022  suceloni 3025  ordnbtwn 3026  onnbtwn 3027  ordsuc 3028  onpwsuc 3030  ordssun 3042  ordequn 3043  ordsucun 3045  ordsucuni 3049  unon 3051  ordunisuc 3052  onsucuni2 3054  suc11 3056  onuninsuc 3071  ordunisuc2 3078  dflim3 3081  nlimon 3085  limuni3 3086  dfom2 3096  nnord 3103  ordom 3104  nnlim 3107  peano5 3116  findes 3123  tfinds 3124  tfindsg2 3126  tfindes 3127  vtoclr 3173  vtoclibr 3175  ralxp 3180  onxpdisj 3203  relssdv 3211  xpsspw 3219  xpexg 3221  coeq1d 3242  coeq2d 3243  dmeqd 3270  rneqd 3300  rnss 3301  dmcoeq 3317  ssres2 3337  resiexg 3347  iss 3348  imaeq1d 3354  imaeq2d 3355  hbimad 3363  imaexg 3367  imasng 3375  iniseg 3381  imass1 3383  imass2 3384  xpsndisj 3419  dmxpss 3422  rnxpss 3423  cores2 3449  relfld 3457  coexg 3465  funssres 3492  fun2ssres 3493  funun 3494  fununi 3503  funcnvuni 3504  fun11uni 3505  funcnvres2 3510  funimaexg 3515  cofunexg 3520  cofunex2g 3521  fnrel 3526  fnco 3535  fnresdm 3536  2elresin 3538  fnssresb 3539  fnima 3544  fn0 3545  fnex 3547  opabex2g 3551  fnopabg 3555  feq1d 3564  ffun 3569  frel 3570  fdm 3571  fss 3574  fco 3575  fssxp 3576  funssxp 3577  ffdm 3578  fcoi1 3584  fcoi2 3585  f00 3596  fconst 3597  fconstg 3598  f1eq1 3599  fofun 3612  fornex 3618  fodmrnu 3619  foconst 3622  f1of 3628  f1ofn 3629  f1ofun 3630  f1orel 3631  f1o5 3636  f1f1orn 3638  f1oabexg 3639  f1ocnv 3640  f1orescnv 3643  f1imacnv 3644  f1ococnv2 3647  f1ococnv1 3648  f1dmex 3649  f1o00 3653  fveq1d 3665  fveq2d 3667  hbfvd 3669  hbfvd2 3670  tz6.12i 3680  elfvdm 3686  nfvres 3687  fnopabfv 3697  fnsnfv 3706  ssimaex 3707  funfv2 3710  fvopab4ndm 3723  fvopab2 3730  fvopab5 3732  fvreseq 3738  elrnopabg 3739  fvelrn 3751  dff4 3755  dff2 3756  dffo3 3758  dffo4 3759  dffo5 3760  exfo 3761  fopab2 3762  fopabco 3771  fopabcos 3772  fsn 3773  fsn2 3775  fnressn 3776  fressnfv 3777  fvconst 3778  fconst2g 3784  fconst3 3789  abrexex 3799  iunexg 3801  f1fv 3813  f1fveq 3815  f1ocnvfv1 3817  f1ocnvfv2 3818  f1ofveu 3821  f1ocnvfv3 3822  f1ocnvdm 3823  cbvfo 3824  isocnv 3835  isotr 3836  isotrALT 3837  isomin 3838  isoini 3839  isofrlem 3840  isofr 3841  isowe 3842  f1oweALT 3845  canth 3846  iunon 3848  tfrlem2 3851  tfrlem5 3854  tfrlem6 3855  tfrlem8 3857  tfrlem9 3858  tfrlem11 3860  tfrlem12 3861  tfrlem13 3862  tfr3 3865  tz7.44lem1 3866  tz7.44-2 3868  tz7.44-3 3869  dfrdg2 3872  rdglem2 3877  rdglim2 3888  frsuct 3892  tz7.48lem 3894  tz7.48-1 3895  tz7.48-2 3896  tz7.48-3 3897  tz7.49 3898  tz7.49c 3899  abianfplem 3900  abianfp 3901  opreq1d 3914  opreq2d 3915  opreqd 3916  hboprd 3921  oprprc1 3923  fnoprabg 3951  oprabex2g 3959  oprabval 3962  oprvalres 3972  oprssoprval 3973  oprvalconst2 3979  oprssdm 3981  ndmoprass 3988  ndmoprdistr 3989  ndmord 3990  ndmordi 3991  caoprmo 4010  2ndval2 4028  curry1 4036  1stcof 4039  eqop 4042  1st2nd 4046  1stdm 4047  2ndrn 4048  dfopab2 4051  dfoprab3 4052  dfoprab5 4053  oe0m1 4098  oa1suc 4102  oesuc 4104  oaordi 4118  oaord 4119  oacan 4120  oaword 4121  oawordri 4122  oawordeulem 4126  oalimcl 4132  oaass 4133  oarec 4134  omordi 4135  omcan 4138  omword 4139  omwordi 4140  omword1 4142  om00 4144  om00el 4145  omlimcl 4147  odi 4148  omass 4149  oneo 4150  oen0 4151  oeordi 4152  oecan 4154  oeword 4155  oewordi 4156  oewordri 4157  oeworde 4158  oelim2 4160  nna0 4161  nnm0 4162  nna0r 4165  nnm0r 4166  nnecl 4169  nnarcl 4170  nnacom 4171  nnmsucr 4178  oaabslem 4189  oaabs 4190  nneob 4193  omsmo 4195  erthdm 4221  ecopqsi 4231  ectocl 4240  ecoptocl 4241  brecop 4244  brecop2 4245  ecopoprdm 4247  ecopoprsym 4248  eceqopreq 4251  th3qlem1 4252  th3qlem2 4253  th3q 4255  oprec 4256  ecoprcom 4257  ecoprass 4258  ecoprdi 4259  pmex 4265  mapex 4266  elmapg 4271  mapval2 4273  map0b 4281  mapsn 4283  mapss 4284  uniixp 4295  ixpexg 4296  ixp0 4299  breng 4311  brdomg 4312  enrefg 4325  domrefg 4328  en2d 4335  idssen 4341  ener 4345  ensymg 4346  domtr 4350  f1imaen 4357  en0 4358  en1 4361  2dom 4362  fundmen 4363  en2sn 4366  snfi 4367  unen 4368  xpsnen 4369  xpsneng 4370  undom 4372  xpcomen 4373  xpdom2 4376  xpdom1 4377  pw2en 4380  sbthlem2 4382  sbthlem4 4384  sbthlem8 4388  sbthlem10 4390  ensdomtr 4405  sdomtr 4408  domsdomtr 4410  enen1 4411  domen1 4413  sdomen1 4415  fodomr 4417  mapenlem2 4422  mapen 4423  mapdom1 4424  mapdom2lem 4425  mapdom2 4426  mapxpen 4427  xpmapenlem3 4430  xpmapenlem5 4432  mapunen 4434  ssenen 4436  phplem1 4440  phplem2 4441  phplem3 4442  phplem4 4443  php 4445  php2 4446  php3 4447  php5 4449  onomeneq 4450  ominf 4460  isfinite1 4462  pssnn 4465  ssfi 4467  domfi 4468  unblem1 4469  unblem2 4470  unblem3 4471  unblem4 4472  unbnn 4473  unfilem1 4476  unfilem3 4478  unfi 4480  unfi2 4481  unifi 4484  unifi2 4485  fiint 4486  abfii3 4489  fodomfi 4492  fodomfib 4493  iunfi 4495  pwfilem 4496  pwfi 4497  pm54.43 4498  supcl 4505  supsnALT 4516  opthreg 4528  inf3lemd 4536  inf3lem5 4541  inf3lem7 4543  infeq5 4545  isfinite 4558  nnsdom 4559  infensuc 4562  noinfep 4564  trcl 4569  zfregs 4571  setind 4572  r1tr 4578  r1ord 4579  r1ord3 4581  r1val1 4582  tz9.12lem3 4585  tz9.12 4586  tz9.13 4587  rankwflem 4589  rankon 4595  rankr1 4598  r1val3 4603  rankval3 4605  bndrank 4606  ranklim 4609  r1pw 4610  r1pwcl 4611  rankuni2 4614  rankun 4615  rankonid 4619  rankr1id 4621  rankuni 4622  rankval4 4626  rankbnd2 4628  rankelun 4631  rankxplim 4636  rankxplim2 4637  rankxplim3 4638  rankxpsuc 4639  scottex 4640  scott0 4641  bnd2 4648  aceq3lem 4656  aceq3 4657  aceq5lem3 4661  aceq5lem4 4662  aceq5lem5 4663  aceq6a 4665  aceq6b 4666  ac7g 4673  ac6lem 4678  ac6 4679  ac6s 4680  ac6s2 4682  ac6s3 4683  ac6s5 4686  kmlem1 4689  kmlem8 4696  kmlem11 4699  kmlem13 4701  numth2 4709  numthcor 4710  weth 4711  zorn2lem2 4713  zorn2lem3 4714  zorn2lem4 4715  zorn2lem5 4716  zorn2lem6 4717  zorn2 4720  zorn 4721  fodom 4722  fodomb 4724  brdom3 4725  brdom4 4727  brdom7disj 4728  brdom6disj 4729  imadomg 4730  unidom 4732  uniimadom 4734  oncardval 4743  oncardon 4744  oncardid 4745  cardnn 4748  cardom 4749  oncard 4753  carden 4755  carddomi 4758  entri3 4764  unxpdom2 4768  sucxpdom 4769  cardlim 4774  cardsdomel 4775  iscard 4776  ondomon 4779  ondomcard 4780  carduni 4781  cardiun 4782  cardmin 4783  alephordi 4797  alephord 4798  alephle 4807  cardaleph 4808  carduniima 4813  cardinfima 4814  alephfplem3 4821  alephfp 4823  alephval2 4825  cfub 4831  cflim 4832  cardcf 4834  cflecard 4835  cfle 4836  cfeq0 4837  cfsuc 4838  cdafi 4859  axrepndlem1 4867  axrepndlem2 4868  axrepnd 4869  axunndlem1 4870  axunnd 4871  axpowndlem2 4873  axpowndlem3 4874  axpowndlem4 4875  axpownd 4876  axregndlem2 4878  axinfndlem1 4880  axinfnd 4881  axacndlem1 4882  axacndlem2 4883  axacndlem3 4884  axacndlem4 4885  axacndlem5 4886  axacnd 4887  zfcndinf 4893  elni2 4928  pion 4930  piord 4931  addpiord 4935  mulpiord 4936  mulclpi 4944  addnidpi 4951  indpi 4957  addcmpblnq 4975  mulcmpblnq 4976  ordpipq 4979  distrpqlem 4989  distrpq 4990  recmulpq 4993  recclpq 4995  recrecpq 4996  dmrecpq 4997  ltsopq 4998  ltapq 4999  ltmpq 5000  ltexpq 5003  halfpq 5005  ltrpq 5008  elnp 5015  genpnnp 5031  genpnmax 5033  mulclprlem 5044  distrlem4pr 5053  1idpr 5056  prlem934a 5060  prlem934b 5061  prlem934 5062  ltexprlem2 5066  ltexprlem4 5068  ltexprlem6 5070  ltexprlem7 5071  ltaprlem 5073  ltapr 5074  reclem1pr 5079  reclem2pr 5080  reclem3pr 5081  reclem4pr 5082  recexpr 5083  suplem2pr 5085  addcmpblnr 5104  mulcmpblnr 5106  ltsrpr 5109  ltsosr 5126  ltasr 5132  recexsrlem 5135  addgt0sr 5136  sqgt0sr 5138  ssgt0sr 5140  mappsrpr 5141  suppsr2 5146  suppsr3 5147  supsrlem1 5148  supsrlem2 5149  mulresr 5180  axaddopr 5188  axmulopr 5189  axmulass 5201  axdistr 5202  recnd 5238  cnegextlem2 5269  cnegextlem3 5270  cnegext 5271  negeqd 5284  hbnegd 5286  renegcl 5339  muladd11t 5345  1re 5358  pnpcant 5401  pnfnre 5419  ltxrltt 5423  xrlenltt 5424  axmulgt0 5429  ltpnft 5466  mnfltt 5467  xrltnsymt 5474  xrlttrt 5477  addge0 5524  mulge0 5532  msqge0 5539  ne0gt0t 5544  ltaddpost 5575  ltnegcon1t 5580  lenegcon1t 5582  lenegcon2t 5583  addge01t 5596  suble0t 5599  recextlem1 5606  recext 5608  muleqaddt 5620  divasst 5655  div0t 5674  divcan5t 5688  divadddivt 5691  divdivdivt 5692  conjmult 5704  redivcl 5705  negeq0t 5713  ltm1t 5722  ltmuldiv 5732  mulgt1t 5752  ltmulgt11t 5753  lemulge11t 5755  lediv1t 5757  lerec 5779  recgt1it 5799  recp1lt1 5800  recrecltt 5801  ledivp1 5805  ltdivp1 5806  posex 5807  nn1suc 5838  nnge1t 5842  nnle1eq1t 5844  nnrecgt0t 5851  nnleltp1t 5852  nnsub 5854  nnaddm1clt 5856  nndivt 5857  nndivtrt 5858  halfaddsubcl 5938  lt2halvest 5940  avglet 5942  lbreu 5943  lble 5945  lbinfm 5946  sup2 5949  infm3lem 5951  suprcl 5953  suprub 5954  suprlub 5955  suprnub 5956  infmrcl 5967  nnreclt 5970  xrsupsslem 5974  xrinfmsslem 5975  xrsupss 5976  xrinfmss 5977  xrub 5978  supxrre 5981  supxrcl 5982  supxrun 5983  infmxrcl 5984  supxrmnf 5985  supxrbnd 5989  supxrgtmnf 5990  supxrbnd1 5993  supxrbnd2 5994  xrsup0 5995  supxrub 5996  supxrleub 5997  nn0le0eq0t 6017  nn0addclt 6018  nn0mulcl 6020  nnnn0addclt 6023  nn0ltp1let 6025  nn0ltlem1t 6027  nnnegz 6036  elnnz 6043  elnn0z 6045  elznn0 6047  elznn 6048  elnnz1 6053  znnnlt1t 6054  nn0subt 6059  nn0negz 6062  peano2zd 6065  elnn0nn 6069  zltp1let 6079  zlem1ltt 6081  zltlem1t 6082  zextlet 6087  recnzt 6089  btwnnzt 6090  gtndivt 6091  nneo 6095  zeot 6097  zneo 6098  zneoOLD 6099  dfuz 6101  uzind 6104  uzind2 6105  uzindOLD 6107  uzwo4OLD 6109  uzwo5OLD 6110  nn0ind-raph 6113  btwnz 6114  uzwo3lem2 6116  zmax 6119  zbtwnre 6120  rebtwnz 6121  flclt 6125  flleltt 6126  flget 6129  flltt 6130  flidt 6131  flval3t 6133  flwordit 6134  fladdzt 6138  flhalft 6140  ceiget 6142  ceim1lt 6143  nnrecret 6166  qbtwnre 6167  qbtwnxr 6168  monoord 6182  om2uzlt2 6187  om2uzran 6188  uzrdgsuc 6192  seq1lem2 6198  seq1val 6200  seq1suclem 6204  seq1m1 6207  seq1rn2 6209  seq1res 6215  ser1recl 6219  ser1p1 6224  ser1mono 6225  ser1add2 6226  ser1add 6227  shftfn 6231  shftf 6239  2shft 6240  seq1shftid 6244  ioo0t 6256  ioossicc 6281  ioonegt 6290  iccnegt 6291  icoshftf1oi 6293  icoshftf1olem 6294  uzidt 6310  uzssz 6313  uzss 6314  eluzp1m1t 6316  eluzaddi 6319  eluzsubi 6320  peano2uzr 6331  uzaddclt 6332  uzind4 6333  uzind4s 6335  uzind4s2 6336  uzwo 6338  uzwoOLD 6339  elfzlem 6356  elfzel1 6364  elfzelz 6365  elfzle1 6366  elfzle2 6367  elfzuz2t 6369  eluzfz1t 6370  elfz3t 6374  elfz1eqt 6375  fznt 6376  fzoptht 6385  fzssp1t 6389  fzp1sst 6390  elfzp1 6393  fznn0t 6399  fzrevralt 6402  fzshftralt 6405  fsequb 6406  fsequb2 6407  limsupvalt 6412  seq0fval 6418  seqzfval 6420  seqzfval2 6421  seqzfn 6422  seqzvalt 6423  seq1seqz 6424  seq1seq02t 6426  seqz1 6430  seqzp1 6431  seqzm1 6432  seq0p1 6434  seqzval2t 6436  seqzfveq 6437  seqzeq 6438  seqzrn 6440  seqzcl 6441  seqzres 6443  seqzres2 6444  ser0cl1 6447  ser0p1 6450  expvalt 6453  expnnvalt 6455  exp1t 6456  expcllem 6458  expm1t 6466  expgt0t 6471  expge0t 6473  expgt1t 6474  expge1t 6475  mulexpt 6476  recexpt 6477  expaddt 6478  expmult 6479  expordit 6482  expword2it 6487  expubndt 6490  sqnegt 6492  sqgt0t 6504  sqlecant 6523  subsq2t 6525  bernneq 6534  bernneq2 6535  expnbndt 6536  discrlem2 6538  discrlem3 6539  nnesq 6543  nn0opthlem2 6546  sqrval 6552  sqr0 6553  sqrlem6 6559  sqrlem12 6565  sqrlem13 6566  sqrlem17 6570  sqrlem18 6571  sqrge0 6583  sqsqr 6602  sqr2irr 6610  crutOLD 6620  crrecz 6623  rimul 6626  reclt 6639  imclt 6640  replimt 6643  replimtOLD 6644  crret 6653  crretOLD 6654  crimt 6655  crimtOLD 6656  imret 6661  reim0t 6662  reim0bt 6663  cjexpt 6703  recjt 6704  imcjt 6705  cjreimt 6714  cjreim2t 6715  cj11t 6716  absnegt 6718  abscjt 6720  sqabsaddt 6734  sqabssubt 6735  absreimsqt 6742  absreimt 6743  absdivz 6745  absnidt 6749  leabst 6750  absret 6752  absresqt 6753  absexpt 6754  absrelet 6755  absimlet 6756  leabs 6758  nn0absclt 6767  lenegsqt 6774  releabst 6775  cjdiv 6777  abs3lem 6789  abs2dift 6790  abs2difabst 6791  abs1m 6792  seq1bnd 6798  seq1ublem 6799  seq1ub 6800  cau2 6801  cau3i 6802  cau5i 6805  cvg1i 6808  cvg2 6810  cvg3 6811  cvganz 6812  caubnd 6814  caure 6815  cauim 6816  ser1absdiflem 6817  facp1t 6824  facne0t 6829  facdivt 6830  facndivt 6831  facwordit 6832  faclbnd 6833  faclbnd2 6834  faclbnd3 6835  faclbnd4lem1 6836  faclbnd4lem3 6838  faclbnd4lem4 6839  faclbnd5 6841  faclbnd6 6842  facavgt 6843  bccmplt 6851  bcn0t 6852  bcnnt 6853  bcnp11t 6854  bcnp1nt 6855  bcpasc 6858  bccl2t 6860  bcclt 6861  permnnt 6862  sumeq2 6874  sumeq1d 6879  sumeq2d 6880  sumeq2dv 6881  2sumeq2dv 6883  sumeqfv 6886  fsumserz 6888  serzfsum 6893  fsum1 6894  fsump1 6895  fsump1s 6902  fsumcllem 6903  fsum1ps 6907  fsum1p 6908  fsumsplit 6909  fsum0split 6910  fsumadd 6911  fsum2 6912  fsum3 6913  fsum4 6914  fsumcom 6917  fsumrev 6918  fsumshft 6920  fsummulc1 6922  fsumconst 6927  fsum0 6928  fsumcmp 6929  fsumcmpndx2 6931  fsumabs 6932  fsumabs2mul 6933  ser1ser0 6937  serzref 6940  serz1p 6941  serz0 6942  serzcmp0 6944  serzsplit 6945  serzmulc 6947  serzrelem 6950  binomlem1 6955  binomlem2 6956  binomlem3 6957  binomlem4 6958  binomlem5 6959  binom1p 6962  bcxmas 6965  clm4 6969  clm4le 6970  clm0 6972  clm0nns 6974  clmi1 6975  clmi2 6976  clm0i 6978  climconst 6982  climconst3 6984  2climnn 6990  2climnn0 6991  climshft 6992  climshft2 6994  iserzshft2 6995  serzclim0 6997  climrecl 6998  climge0 7000  climaddlem3 7003  climmullem1 7007  climmullem2 7008  climmullem3 7009  climmullem4 7010  climmullem5 7011  climmullem8 7014  clim2serzt 7021  climcmplem 7024  climsqueeze 7027  climsqueeze2 7028  iserzcmp 7029  clim2serz 7032  iserzex 7033  climserzle 7034  climabslem 7035  climcj 7037  climre 7038  climim 7039  climubi 7040  climsup 7042  climcau 7043  caucvglem2 7045  caucvglem6 7049  caucvg 7050  caucvg3a 7051  caucvg3lem 7053  caucvg3t 7055  serzf0 7056  ser1f0 7057  ser1const 7058  ser10 7059  ser1clim0 7060  ser1cmp 7061  ser1cmp2lem 7063  ser1cmp2 7064  iserzabslem 7065  cvgcmp2lem 7067  cvgcmp2clem 7069  cvgcmp3c