Theorem syl 14

Description: An inference version of the transitive laws for implication imim2 54 and imim1 75, 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." (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 20-Oct-2011.) (Proof shortened by Wolf Lammen, 26-Jul-2012.)

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	. . 3 |- ( ps -> ch )
3	2	a1i 9	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mpd 13	1 |- ( ph -> ch )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  3syl  17  4syl  18  a1d  22  a2d  26  sylcom  28  syl11  31  syl2im  38  sylsyld  57  pm2.86i  97  simpld  110  simprd  112  sylbi  119  sylib  120  sylibr  132  sylbir  133  biimpd  142  biantrud  298  biantrurd  299  pm2.01d  580  pm2.21d  581  pm2.24d  584  notnotd  592  pm5.21nii  652  ord  675  orcoms  681  orcd  684  orcs  686  biortn  696  pm4.67dc  814  annimim  815  imordc  829  pm4.54dc  838  pm4.55dc  879  dn1dc  901  dedlem0a  909  oplem1  916  simp1d  950  simp2d  951  simp3d  952  3adant1  956  3adant2  957  3adant3  958  3mix1d  1113  3mix2d  1114  3mix3d  1115  syl12anc  1167  syl21anc  1168  syl3anc  1169  syl3an1  1202  syl3an  1211  mp3an12i  1272  ecased  1280  xornbi  1317  pm5.15dc  1320  anxordi  1331  mpisyl  1375  a7s  1383  al2imi  1387  alimdh  1396  alrimih  1398  alcoms  1405  hbal  1406  albidh  1409  alequcoms  1449  nalequcoms  1450  nfrd  1453  sps  1470  hbor  1478  19.21bi  1490  nford  1499  nfand  1500  hbimd  1505  19.23bi  1523  exbi  1535  eximdh  1542  exbidh  1545  19.29  1551  19.29r2  1553  19.29x  1554  19.35-1  1555  19.25  1557  19.40-2  1563  i19.24  1570  i19.39  1571  alexim  1576  exanaliim  1578  hbnt  1583  hbnd  1585  nfnd  1587  19.9d  1591  19.36i  1602  19.41h  1615  ax9o  1628  equcoms  1634  ax10  1645  hbae  1646  hbaes  1648  hbnaes  1651  naecoms  1652  equs4  1653  equsexd  1657  spimt  1664  spimh  1665  cbv1h  1673  cbv2  1675  equvini  1681  equveli  1682  nfald  1683  nfexd  1684  stdpc4  1698  sbh  1699  equs5e  1716  ax10oe  1718  sb4a  1722  equs45f  1723  sb6f  1724  sb4e  1726  hbsb2a  1727  hbsb2e  1728  hbsb3  1729  ax16  1734  dveeq2  1736  ax11v2  1741  equs5or  1751  sbequi  1760  spsbe  1763  spsbim  1764  sbbidh  1766  sbbid  1767  sbidm  1772  ax16i  1779  sbi2v  1813  cbvexdh  1842  nfsbt  1891  sbalyz  1916  dvelimdf  1933  sbal2  1939  mo23  1982  mor  1983  modc  1984  eu2  1985  mo3h  1994  euor2  1999  moexexdc  2025  2eu2ex  2030  bamalip  2062  bm1.1  2066  eqeq1d  2089  eqeq2d  2092  eleq1d  2147  eleq2d  2148  nfcrd  2232  dcned  2251  neeq1d  2263  neeq2d  2264  neleq12d  2345  ral2imi  2427  rexim  2455  reximdai  2459  r19.12  2466  rexlimd2  2475  r19.29  2494  r19.29d2r  2499  r19.29vva  2500  r19.35-1  2504  r19.36av  2505  raleqdv  2555  rexeqdv  2556  rabeqbidv  2596  rabeqbidva  2597  elexd  2612  cgsexg  2634  cgsex2g  2635  cgsex4g  2636  vtoclgft  2649  vtoclgf  2657  vtocleg  2669  spcgft  2675  spcegft  2677  spc3gv  2690  rspct  2694  rspc2ev  2715  eqvincg  2719  pm13.183  2732  dedhb  2761  eueq3dc  2766  mosubt  2769  mob  2774  morex  2776  euind  2779  reuind  2795  sbceq1d  2820  sbcco2  2837  sbceqal  2869  sbcabel  2895  spesbcd  2900  rmo2i  2904  csbeq1d  2914  csbvarg  2933  sbcnestgf  2953  csbidmg  2958  csbco3g  2960  sseldi  2997  sseld  2998  sseq1d  3026  sseq2d  3027  uniiunlem  3082  difeq1d  3089  difeq2d  3090  difss2d  3101  ssdifd  3108  sscond  3109  ssdifssd  3110  uneq1d  3125  uneq2d  3126  ineq1d  3166  ineq2d  3167  uneqin  3215  reuss2  3244  reupick2  3250  eq0rdv  3288  ssdisj  3300  uneqdifeqim  3328  ralm  3345  iftrued  3358  iffalsed  3361  ifsbdc  3363  ifeq1d  3366  ifeq2d  3367  ifbid  3370  ifcldadc  3378  ifeq1dadc  3379  ifbothdc  3380  pweqd  3387  elpwid  3392  sneqd  3411  elpr2  3420  rabsnt  3467  preq1d  3475  preq2d  3476  tpeq1d  3481  tpeq2d  3482  tpeq3d  3483  snnzg  3507  snmg  3508  prmg  3511  snssd  3530  opeq1d  3576  opeq2d  3577  oteq1d  3582  oteq2d  3583  oteq3d  3584  opprc1  3592  opprc2  3593  oprcl  3594  unieqd  3612  unissd  3625  inteqd  3641  intmin3  3663  intmin4  3664  intab  3665  ss2iun  3693  iineq2  3695  iineq2d  3698  iuneq2dv  3699  iuneq1d  3701  dfiin2g  3711  ssiun  3720  iinss  3729  riinm  3750  disjss2  3769  disjeq2  3770  disjeq2dv  3771  disjss1  3772  disjeq1  3773  disjeq1d  3774  invdisj  3780  breq1d  3795  breqd  3796  breq2d  3797  mpteq1d  3863  triun  3888  trint  3890  repizf  3894  a9evsep  3900  nalset  3908  elssabg  3923  inteximm  3924  iinexgm  3929  pwne  3934  class2seteq  3937  bnd2  3947  abssexg  3955  snexg  3956  prelpwi  3969  rext  3970  pwel  3973  exss  3982  opexg  3983  opm  3989  opth1  3991  opth  3992  copsex2t  4000  copsex2g  4001  0nelop  4003  moop2  4006  opelopabsb  4015  ssopab2dv  4033  pwssunim  4039  poeq2  4055  sotritric  4079  sotritrieq  4080  sess1  4092  sess2  4093  seeq1  4094  seeq2  4095  frirrg  4105  onelss  4142  ordtr1  4143  ontr1  4144  limuni2  4152  trsuc  4177  tpexg  4197  eusvnf  4203  eusvnfb  4204  ralxfr2d  4214  rexxfr2d  4215  ralxfrALT  4217  reuhypd  4221  eldifpw  4226  iunpw  4229  ssorduni  4231  ssonuni  4232  onun2  4234  onss  4237  orduni  4239  bm2.5ii  4240  ordsucim  4244  suceloni  4245  sucelon  4247  ordsucss  4248  onsucsssucr  4253  sucunielr  4254  onintonm  4261  ordtriexmidlem  4263  ordtri2orexmid  4266  ordtri2or2exmidlem  4269  onsucsssucexmid  4270  ordsucunielexmid  4274  regexmidlem1  4276  reg2exmidlema  4277  elirr  4284  ordn2lp  4288  en2lp  4297  opthreg  4299  ordsoexmid  4305  ordsuc  4306  onsucuni2  4307  ordpwsucss  4310  onnmin  4311  onintexmid  4315  ordwe  4318  wetriext  4319  wessep  4320  reg3exmidlemwe  4321  tfi  4323  tfisi  4328  peano2  4336  peano5  4339  findes  4344  nnord  4352  peano2b  4355  nn0eln0  4359  xpeq1d  4386  xpeq2d  4387  otelxp1  4397  mosubopt  4423  releqd  4442  relssdv  4450  xpsspw  4468  xpiindim  4491  relop  4504  ideqg  4505  coeq1d  4515  coeq2d  4516  cnveqd  4529  dmeqd  4555  rneqd  4581  rnss  4582  dmiin  4598  elrnmptg  4604  riinint  4611  dmrnssfld  4613  dmcosseq  4621  dmcoeq  4622  reseq1d  4629  reseq2d  4630  ssres2  4656  imaeq1d  4687  imaeq2d  4688  imasng  4710  elreimasng  4711  iniseg  4717  imass1  4720  imass2  4721  issref  4727  poirr2  4737  xpsndisj  4769  xpima1  4787  xpimasn  4789  opswapg  4827  elxp4  4828  elxp5  4829  relcoi1  4869  cnviinm  4879  iotaval  4898  iotanul  4902  iota4  4905  iota4an  4906  iotabidv  4908  iota2df  4911  funmo  4937  funss  4940  funeq  4941  funeqd  4943  funeu  4946  funco  4960  funun  4964  funcnvsn  4965  funprg  4969  funtpg  4970  fntpg  4975  fununi  4987  funcnvuni  4988  fun11uni  4989  funcnvres2  4994  imadiflem  4998  funimaexglem  5002  fneq1d  5009  fneq2d  5010  fnrel  5017  fneu  5023  fnco  5027  fnresdm  5028  2elresin  5030  fnssresb  5031  feq1d  5054  feq2d  5055  feq123d  5057  ffun  5068  frel  5069  fdm  5070  fco2  5077  fssxp  5078  ffdm  5081  fresin  5088  fcoi1  5090  fcoi2  5091  dmfex  5099  f00  5101  fnconstg  5104  f1fn  5113  f1fun  5114  f1rel  5115  f1dm  5116  f1ssres  5119  fofun  5127  fofn  5128  foima  5131  f1eq123d  5141  foeq123d  5142  f1oeq123d  5143  f1of  5146  f1ofn  5147  f1ofun  5148  f1orel  5149  f1odm  5150  f1ores  5161  f1orescnv  5162  f1imacnv  5163  foimacnv  5164  fun11iun  5167  resdif  5168  f1cnv  5170  fococnv2  5172  f1ococnv2  5173  f1cocnv2  5174  f1ococnv1  5175  f1cocnv1  5176  f1o00  5181  fo00  5182  f1osng  5187  brprcneu  5191  fvprc  5192  fveq1d  5200  fveq2d  5202  fvssunirng  5210  relfvssunirn  5211  funfvex  5212  fvexg  5214  sefvex  5216  relelfvdm  5226  nfvres  5227  nfunsn  5228  fnbrfvb  5235  funbrfv2b  5239  fvelrnb  5242  feqmptd  5247  fniinfv  5252  ssimaex  5255  funfvdm  5257  fvun1  5260  dmfco  5262  fvco2  5263  fvmptssdm  5276  fvmptdf  5279  fvmptdv2  5281  mpteqb  5282  eqfnfv  5286  fvreseq  5292  fndmdif  5293  fndmin  5295  chfnrn  5299  fvimacnvi  5302  fvimacnv  5303  fniniseg  5308  fniniseg2  5310  inpreima  5314  difpreima  5315  respreima  5316  fvelrn  5319  elrnrexdm  5327  ralrnmpt  5330  rexrnmpt  5331  dff3im  5333  dffo3  5335  dffo4  5336  dffo5  5337  fmpt  5340  f1ompt  5341  fmpt2d  5348  f1oresrab  5350  fmptco  5351  fmptcof  5352  fcompt  5354  fsn  5356  fsng  5357  fsn2  5358  dfmptg  5363  ressnop0  5365  fprg  5367  ftpg  5368  fressnfv  5371  fvconst  5372  fmptap  5374  fmptpr  5376  fvunsng  5378  fsnunf  5383  fsnunfv  5384  fconst3m  5401  resfunexg  5403  eufnfv  5410  fniunfv  5422  elunirn  5426  fnunirn  5427  dff13  5428  f1mpt  5431  f1ocnvfv2  5438  f1ocnvdm  5441  fcof1  5443  cbvfo  5445  cbvexfo  5446  cocan1  5447  fcof1o  5449  foeqcnvco  5450  f1eqcocnv  5451  fliftrel  5452  fliftel  5453  fliftfun  5456  fliftf  5459  isocnv  5471  isocnv2  5472  isores1  5474  isoini  5477  isoini2  5478  isopolem  5481  isopo  5482  isosolem  5483  isoso  5484  f1oiso  5485  riotass2  5514  riotass  5515  eusvobj1  5519  f1ofveu  5520  acexmidlemab  5526  acexmidlemcase  5527  acexmidlem1  5528  acexmidlem2  5529  oveq1d  5547  oveq2d  5548  oveqd  5549  ovprc1  5561  ovprc2  5562  brabvv  5571  ssoprab2  5581  fnoprabg  5622  mpt22eqb  5630  ralrnmpt2  5635  rexrnmpt2  5636  ovmpt2dxf  5646  ovmpt2df  5652  ovi3  5657  ovg  5659  ovres  5660  ovconst2  5672  f1ocnvd  5722  f1ocnv2d  5724  f1opw2  5726  f1opw  5727  suppssfv  5728  suppssov1  5729  offval  5739  ofrfval  5740  ofrval  5742  off  5744  offval2  5746  ofrfval2  5747  suppssof1  5748  ofco  5749  offveqb  5750  caofref  5752  caofinvl  5753  caofrss  5755  caoftrn  5756  cofunexg  5758  cofunex2g  5759  fnexALT  5760  fornex  5762  f1dmex  5763  abrexexg  5765  iunexg  5766  oprabexd  5774  offres  5782  ofmresex  5784  1stexg  5814  2ndexg  5815  op1steq  5825  1st2nd  5827  1stdm  5828  releldm2  5831  sbcopeq1a  5833  csbopeq1a  5834  dfoprab3  5837  eloprabi  5842  mpt2fvex  5849  mpt2exg  5854  fmpt2co  5857  1stconst  5862  2ndconst  5863  f2ndf  5867  fo2ndf  5868  f1o2ndf1  5869  cnvoprab  5875  f1od2  5876  mpt2xopn0yelv  5877  tposss  5884  tposeq  5885  tposeqd  5886  brtpos2  5889  brtposg  5892  tposexg  5896  dftpos4  5901  tposfo2  5905  tposf2  5906  tposf12  5907  2pwuninelg  5921  iunon  5922  issmo2  5927  smoeq  5928  smores  5930  smores2  5932  smodm2  5933  smoiso  5940  tfrlem1  5946  tfrlem5  5953  tfrlem6  5955  tfrlem8  5957  tfrlem9  5958  tfr0  5960  tfrlemisucaccv  5962  tfrlemibfn  5965  tfrlemiubacc  5967  tfrlemiex  5968  tfrexlem  5971  tfri2d  5973  tfri3  5976  rdgeq1  5981  rdgeq2  5982  rdgtfr  5984  rdgruledefgg  5985  rdgivallem  5991  rdgss  5993  rdgisuc1  5994  freceq1  6002  freceq2  6003  frec0g  6006  frectfr  6008  frecfnom  6009  frecsuclem1  6010  frecsuclemdm  6011  frecsuclem2  6012  frecsuclem3  6013  frecrdg  6015  freccl  6016  2oconcl  6045  sucinc2  6049  omfnex  6052  omv  6058  oeiv  6059  oeicl  6065  oav2  6066  oasuc  6067  oa1suc  6070  oawordi  6072  nna0  6076  nnm0  6077  nnacom  6086  nnaass  6087  nndi  6088  nnmass  6089  nnmsucr  6090  nnsucelsuc  6093  nnsucsssuc  6094  nntri3or  6095  nntri1  6097  nntri2or2  6099  nndceq  6100  nndcel  6101  nnsseleq  6102  nndifsnid  6103  nnaordi  6104  nnaord  6105  nnaword  6107  nnaordex  6123  nnm00  6125  ecexr  6134  ercl  6140  ersym  6141  ertr  6144  erref  6149  erssxp  6152  iserd  6155  brdifun  6156  swoer  6157  swoord1  6158  eceq1d  6165  ecss  6170  ereldm  6172  erth  6173  ecelqsg  6182  ecopqsi  6184  uniqs  6187  uniqs2  6189  elqsn0  6198  xpiderm  6200  iinerm  6201  riinerm  6202  ecinxp  6204  ecoptocl  6216  erovlem  6221  eroprf  6222  ecopovsym  6225  ecopover  6227  ecopovsymg  6228  ecopoverg  6230  th3qlem2  6232  th3q  6234  bren  6251  brdomg  6252  brdomi  6253  domrefg  6270  dom3d  6277  ener  6282  ensymd  6286  domtr  6288  f1imaen2g  6296  en0  6298  en1  6302  en1bg  6303  en1uniel  6307  2dom  6308  fundmen  6309  enm  6317  xpsnen  6318  xpcomco  6323  xpdom2  6328  xpdom3m  6331  fopwdom  6333  phplem1  6338  phplem2  6339  phplem3  6340  phplem4  6341  phplem4dom  6348  nndomo  6350  phpm  6351  phpelm  6352  phplem4on  6353  fidceq  6354  fidifsnen  6355  fidifsnid  6356  ssfilem  6360  dif1en  6364  php5fin  6366  fin0  6369  fin0or  6370  diffitest  6371  findcard2  6373  findcard2s  6374  ac6sfi  6379  en2eqpr  6380  nnwetri  6382  onunsnss  6383  unsnfi  6384  unsnfidcex  6385  unsnfidcel  6386  f1dmvrnfibi  6393  f1vrnfibi  6394  supeq1d  6400  supval2ti  6408  supclti  6411  supubti  6412  suplubti  6413  supelti  6415  supsnti  6418  isotilem  6419  isoti  6420  supisolem  6421  supisoex  6422  supisoti  6423  infeq1d  6425  infeq3  6428  ordiso2  6446  isnumi  6451  oncardval  6455  carden2bex  6458  pm54.43  6459  pr2ne  6461  pion  6500  piord  6501  elni2  6504  addpiord  6506  mulpiord  6507  mulidpi  6508  ltsopi  6510  mulclpi  6518  addnidpig  6526  indpi  6532  dfplpq2  6544  addcmpblnq  6557  mulcmpblnq  6558  dmaddpqlem  6567  nqpi  6568  dmaddpq  6569  dmmulpq  6570  mulcanenq  6575  distrnqg  6577  recexnq  6580  ltdcnq  6587  ltexnqq  6598  halfnq  6601  nsmallnqq  6602  nsmallnq  6603  subhalfnqq  6604  archnqq  6607  prarloclemarch  6608  prarloclemarch2  6609  ltrnqg  6610  ltrnqi  6611  nnnq  6612  ltnnnq  6613  enq0sym  6622  enq0ref  6623  enq0tr  6624  nqnq0pi  6628  nqnq0  6631  nq0nn  6632  addcmpblnq0  6633  mulcmpblnq0  6634  mulcanenq0ec  6635  addnq0mo  6637  mulnq0mo  6638  addnnnq0  6639  mulnnnq0  6640  nqpnq0nq  6643  nqnq0a  6644  nqnq0m  6645  nq0m0r  6646  nq0a0  6647  distrnq0  6649  addassnq0  6652  nq02m  6655  preqlu  6662  elinp  6664  prop  6665  prnmaddl  6680  prarloclemlt  6683  prarloclemlo  6684  prarloclem3  6687  prarloclemn  6689  prarloclem5  6690  prarloclemcalc  6692  prarloc  6693  genpml  6707  genpmu  6708  genprndl  6711  genprndu  6712  genpdisj  6713  genpassl  6714  genpassu  6715  addnqprllem  6717  addnqprulem  6718  addnqprl  6719  addnqpru  6720  addlocprlemlt  6721  addlocprlemeqgt  6722  addlocprlemeq  6723  addlocprlemgt  6724  addlocprlem  6725  nqprm  6732  nqprloc  6735  nnprlu  6743  addnqprlemrl  6747  addnqprlemru  6748  addnqprlemfl  6749  addnqprlemfu  6750  addnqpr  6751  appdivnq  6753  appdiv0nq  6754  prmuloclemcalc  6755  mulnqprl  6758  mulnqpru  6759  mullocprlem  6760  mullocpr  6761  mulnqprlemrl  6763  mulnqprlemru  6764  mulnqprlemfl  6765  mulnqprlemfu  6766  mulnqpr  6767  ltprordil  6779  1idprl  6780  1idpru  6781  ltnqpri  6784  ltaddpr  6787  ltexprlemm  6790  ltexprlemlol  6792  ltexprlemopu  6793  ltexprlemupu  6794  ltexprlemdisj  6796  ltexprlemloc  6797  ltexprlemfl  6799  ltexprlemrl  6800  ltexprlemfu  6801  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  lteupri  6807  prplnqu  6810  recexprlemell  6812  recexprlemelu  6813  recexprlemm  6814  recexprlemdisj  6820  recexprlemloc  6821  recexprlem1ssl  6823  recexprlem1ssu  6824  recexprlemss1l  6825  recexprlemss1u  6826  aptiprlemu  6830  ltmprr  6832  archpr  6833  caucvgprlemcanl  6834  cauappcvgprlemm  6835  cauappcvgprlemdisj  6841  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlemladd  6848  cauappcvgprlem1  6849  cauappcvgprlem2  6850  archrecnq  6853  archrecpr  6854  caucvgprlemk  6855  caucvgprlemm  6858  caucvgprlemloc  6865  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlem1  6869  caucvgprlem2  6870  caucvgprprlemloccalc  6874  caucvgprprlemnkltj  6879  caucvgprprlemnkeqj  6880  caucvgprprlemnjltk  6881  caucvgprprlemnbj  6883  caucvgprprlemml  6884  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemupu  6890  caucvgprprlemloc  6893  caucvgprprlemexbt  6896  caucvgprprlemexb  6897  caucvgprprlemaddq  6898  caucvgprprlem1  6899  caucvgprprlem2  6900  addcmpblnr  6916  addsrmo  6920  mulsrmo  6921  addsrpr  6922  mulsrpr  6923  recexgt0sr  6950  recexsrlem  6951  addgt0sr  6952  archsr  6958  srpospr  6959  prsrriota  6964  caucvgsrlemcl  6965  caucvgsrlemasr  6966  caucvgsrlemcau  6969  caucvgsrlemgt1  6971  caucvgsrlemoffval  6972  caucvgsrlemoffres  6976  caucvgsr  6978  elreal2  6999  mulresr  7006  addcnsrec  7010  mulcnsrec  7011  pitonnlem2  7015  pitonn  7016  pitore  7018  recnnre  7019  peano2nnnn  7021  ltrennb  7022  recidpipr  7024  recidpirqlemcalc  7025  recidpirq  7026  axaddcl  7032  axmulcl  7034  axrnegex  7045  rereceu  7055  recriota  7056  peano5nnnn  7058  nntopi  7060  axcaucvglemcl  7061  axcaucvglemcau  7064  axcaucvglemres  7065  mulid1  7116  mulid1d  7136  mulid2d  7137  recnd  7147  renepnfd  7169  renemnfd  7170  xrlenlt  7177  ltxrlt  7178  ltnrd  7222  readdcan  7248  addid1d  7257  addid2d  7258  cnegexlem3  7285  cnegex  7286  addcan  7288  addcan2  7289  subval  7300  negeqd  7303  subcl  7307  negcld  7406  subidd  7407  subid1d  7408  negidd  7409  negnegd  7410  negeq0d  7411  negrebd  7418  renegcld  7484  negf1o  7486  mul02lem2  7492  mul02d  7496  mul01d  7497  mulm1d  7514  lt0ne0d  7614  leidd  7615  lt0neg1d  7616  lt0neg2d  7617  le0neg1d  7618  le0neg2d  7619  recexre  7678  msqge0d  7718  mulge0  7719  leltap  7724  ap0gt0  7738  recexap  7743  muleqadd  7758  divvalap  7762  divclap  7766  divmulasscomap  7784  muldivdirap  7795  eqnegd  7821  div1d  7868  recgt1i  7976  recp1lt1  7977  recreclt  7978  ledivp1  7981  ltp1d  8008  lep1d  8009  ltm1d  8010  lem1d  8011  lbreu  8023  lbcl  8024  lble  8025  creur  8036  creui  8037  cju  8038  peano5nni  8042  peano2nn  8051  peano2nnd  8054  nn1suc  8058  nnge1  8062  nnrecgt0  8076  nnge1d  8081  nngt0d  8082  nnne0d  8083  nnap0d  8084  nnrecred  8085  halfpos  8262  halfaddsubcl  8264  lt2halves  8266  nominpos  8268  avglt1  8269  avglt2  8270  avgle1  8271  avgle2  8272  2timesd  8273  times2d  8274  halfcld  8275  2halvesd  8276  rehalfcld  8277  xp1d2m1eqxm1d2  8283  div4p1lem1div2  8284  nnrecl  8286  bndndx  8287  nnm1nn0  8329  elnnnn0c  8333  nn0supp  8340  nn0ge0d  8344  nn0ge2m1nn  8348  elnn0z  8364  elnnz1  8374  nn0negz  8385  peano2zm  8389  ztri3or  8394  zltp1le  8405  nn0n0n1ge2  8418  zdceq  8423  zdcle  8424  zdclt  8425  nn0n0n1ge2b  8427  nn0lt10b  8428  nn0ge0div  8434  zdiv  8435  recnz  8440  btwnnz  8441  suprzclex  8445  zneo  8448  nneoor  8449  nneo  8450  zeo  8452  zeo2  8453  peano5uzti  8455  uzind2  8459  nn0ind-raph  8464  zindd  8465  btwnz  8466  znegcld  8471  peano2zd  8472  uzn0  8634  uzss  8639  eluzp1m1  8642  eluzaddi  8645  eluzsubi  8646  eluzadd  8647  eluzsub  8648  uzin  8651  peano2uzr  8673  uzind4  8676  supinfneg  8683  infsupneg  8684  supminfex  8685  elnn1uz2  8694  indstr2  8696  ublbneg  8698  negm  8700  lbzbi  8701  nn01to3  8702  nn0ge2m1nnALT  8703  divfnzn  8706  qapne  8724  rpne0  8749  difrp  8770  nnrpd  8772  rpgt0d  8776  rpge0d  8777  rpne0d  8778  rpap0d  8779  rpreccld  8784  rphalfcld  8786  reclt1d  8787  recgt1d  8788  divge1  8800  ledivge1le  8803  nn0ledivnn  8838  xrltnsym  8868  xrlttr  8870  xrltso  8871  xrlttri3  8872  nltpnft  8884  ngtmnft  8885  rexneg  8897  xnegneg  8900  xltnegi  8902  xnegcld  8909  ixxdisj  8926  eliooord  8951  elioc2  8959  elico2  8960  elicc2  8961  icodisj  9014  ioodisj  9015  iccf1o  9026  elfzel2  9043  elfzel1  9044  elfzelz  9045  elfzle1  9046  elfzle2  9047  elfzle3  9049  eluzfz1  9050  eluzfz2  9051  elfz3  9053  elfzubelfz  9055  fzm  9057  fzsplit2  9069  fzsplit  9070  fz01en  9072  elfz1end  9074  fznn0sub  9075  fzmmmeqm  9076  fzopth  9079  fzsuc  9086  fzpred  9087  elfzp1  9089  fzp1elp1  9092  fznatpl1  9093  fzpr  9094  fztp  9095  fzsuc2  9096  fzp1disj  9097  fzdifsuc  9098  fztpval  9100  fzrev3i  9105  elfz1b  9107  uzdisj  9110  fseq1p1m1  9111  fseq1m1p1  9112  fzm1  9117  fzneuz  9118  fznuz  9119  fzrevral  9122  fzshftral  9125  ige2m1fz  9127  elfz0add  9134  elfz0fzfz0  9137  uzsubfz0  9140  elfzmlbm  9142  elfzmlbp  9143  difelfznle  9146  nn0split  9147  nn0disj  9148  2ffzeq  9151  elfzo3  9172  fzonnsub2  9179  fzoss2  9181  fzossrbm1  9182  fzosplit  9186  fzo1fzo0n0  9192  fzonmapblen  9196  fzofzim  9197  fzocatel  9208  ubmelfzo  9209  elfzodifsumelfzo  9210  elfzom1elp1fzo  9211  fzval3  9213  zpnn0elfzo  9216  fzosplitsnm1  9218  fzossfzop1  9221  fzo0sn0fzo1  9230  fzoend  9231  ssfzo12  9233  ssfzo12bi  9234  ubmelm1fzo  9235  fzofzp1  9236  fzofzp1b  9237  elfzom1b  9238  peano2fzor  9241  fzosplitsn  9242  fzosplitprm1  9243  fzisfzounsn  9245  fzostep1  9246  fzoshftral  9247  exfzdc  9249  subfzo0  9251  qdceq  9256  qbtwnzlemex  9259  rebtwn2z  9263  qbtwnre  9265  qbtwnxr  9266  ioo0  9268  ico0  9270  ioc0  9271  flqcl  9277  flqlelt  9278  flqcld  9279  flqlt  9285  flid  9286  flqidm  9287  flqltnz  9289  flqwordi  9290  flqbi  9292  adddivflid  9294  flqmulnn0  9301  flhalf  9304  fldivnn0le  9305  flltdivnn0lt  9306  fldiv4p1lem1div2  9307  ceilqval  9308  ceiqge  9311  ceiqm1l  9313  ceiqle  9315  ceilid  9317  flqeqceilz  9320  intfracq  9322  flqdiv  9323  modqcl  9328  flqpmodeq  9329  modq0  9331  mulqmod0  9332  negqmod0  9333  modqge0  9334  modqlt  9335  modqelico  9336  zmod10  9342  modqmulnn  9344  zmodfzo  9349  zmodid2  9354  zmodidfzo  9355  modqabs  9359  modqabs2  9360  modqcyc  9361  modqadd1  9363  modqaddabs  9364  mulp1mod1  9367  modqmuladd  9368  modqmuladdim  9369  modqmuladdnn0  9370  qnegmod  9371  m1modge3gt1  9373  addmodid  9374  modqadd2mod  9376  modqm1p1mod0  9377  modqltm1p1mod  9378  modqmul1  9379  modqmul12d  9380  modqnegd  9381  modqadd12d  9382  modqsub12d  9383  q2submod  9387  modifeq2int  9388  modaddmodup  9389  modaddmodlo  9390  modqmulmodr  9392  modqaddmulmod  9393  modqdi  9394  modqsubdir  9395  modqeqmodmin  9396  modfzo0difsn  9397  modsumfzodifsn  9398  addmodlteq  9400  frec2uz0d  9401  frec2uzsucd  9403  frec2uzuzd  9404  frec2uzrand  9407  frec2uzf1od  9408  frecuzrdgrrn  9410  frec2uzrdg  9411  frecuzrdgrom  9412  frecuzrdgfn  9414  frecuzrdgcl  9415  frecuzrdg0  9416  frecuzrdgsuc  9417  uzenom  9418  frecfzennn  9419  fzfig  9422  uzsinds  9428  iseqeq1  9434  iseqeq2  9435  iseqeq4  9437  iseqovex  9439  iseqval  9440  iseqfn  9441  iseq1  9442  iseqcl  9443  iseqp1  9445  iseqm1  9447  iseqfveq2  9448  iseqfeq2  9449  iseqfveq  9450  iseqshft2  9452  monoord  9455  monoord2  9456  isermono  9457  iseqsplit  9458  iseq1p  9459  iseqcaopr3  9460  iseqid3  9465  iseqid3s  9466  iseqid  9467  iseqhomo  9468  iseqz  9469  serige0  9473  serile  9474  expival  9478  expnegap0  9484  expcllem  9487  qexpclz  9497  m1expcl2  9498  1exp  9505  expge0  9512  expge1  9513  expgt1  9514  mulexp  9515  exprecap  9517  expaddzaplem  9519  expaddzap  9520  expmul  9521  m1expeven  9523  leexp2r  9530  exple1  9532  expubnd  9533  sqneg  9535  sqsubswap  9536  sqdivap  9540  sqgt0ap  9544  nnsqcl  9545  qsqcl  9547  sq11  9548  sqge0  9552  zsqcl2  9553  sumsqeq0  9554  sq0id  9568  nnlesq  9578  iexpcyc  9579  subsq2  9582  binom2  9585  binom3  9590  zesq  9591  nnesq  9592  bernneq  9593  bernneq3  9595  expnbnd  9596  exp0d  9599  exp1d  9600  sqvald  9602  sqcld  9603  0expd  9621  sqoddm1div8  9625  nnsqcld  9626  resqcld  9631  sqge0d  9632  facnn  9654  fac0  9655  fac1  9656  facp1  9657  faccld  9663  facndiv  9666  facwordi  9667  faclbnd  9668  faclbnd6  9671  facavg  9673  bcval  9676  bcrpcl  9680  bccmpl  9681  bcn0  9682  bcn1  9685  bcnp1n  9686  bcm1k  9687  bcp1n  9688  bcp1nk  9689  ibcval5  9690  bcn2  9691  bcp1m1  9692  bcpasc  9693  bccl  9694  bcn2m1  9696  permnn  9698  shftlem  9704  shftfvalg  9706  shftfibg  9708  shftdm  9710  shftfib  9711  shftfn  9712  shftval  9713  2shfti  9719  cjval  9732  cjth  9733  cjf  9734  imval  9737  reim  9739  imcl  9741  crre  9744  crim  9745  replim  9746  remim  9747  reim0  9748  mulreap  9751  rere  9752  remullem  9758  redivap  9761  imdivap  9768  cjcj  9770  cjadd  9771  cjmulrcl  9774  cjmulval  9775  cjneg  9777  addcj  9778  cjexp  9780  imval2  9781  cjreim2  9791  cjdivap  9796  recld  9825  imcld  9826  cjcld  9827  replimd  9828  remimd  9829  cjcjd  9830  reim0bd  9831  rerebd  9832  cjrebd  9833  cjne0d  9834  cjap0d  9835  recjd  9836  imcjd  9837  cjmulrcld  9838  cjmulvald  9839  cjmulge0d  9840  renegd  9841  imnegd  9842  cjnegd  9843  addcjd  9844  rered  9856  reim0d  9857  cjred  9858  caucvgrelemcau  9866  caucvgre  9867  cvg1nlemres  9871  cvg1n  9872  r19.29uz  9878  recvguniq  9881  rennim  9888  sqrt0rlem  9889  resqrexlemover  9896  resqrexlemcalc3  9902  resqrexlemnm  9904  resqrexlemcvg  9905  resqrexlemgt0  9906  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemga  9909  resqrtcl  9915  sqrtsq  9930  absneg  9936  abscj  9938  sqabsadd  9941  sqabssub  9942  absrpclap  9947  abs00ad  9951  abs00bd  9952  absreimsq  9953  absreim  9954  absmul  9955  absdivap  9956  absid  9957  absnid  9959  leabs  9960  qabsord  9962  absre  9963  absresq  9964  absrele  9969  absimle  9970  ltabs  9973  abslt  9974  absle  9975  abssubap0  9976  lenegsq  9981  releabs  9982  recvalap  9983  nnabscl  9986  abssub  9987  abstri  9990  abs2dif  9992  abs2difabs  9994  abs3lem  9997  cau3lem  10000  cau4  10002  caubnd2  10003  rpsqrtcld  10044  leabsd  10047  absred  10048  abscld  10067  absvalsqd  10068  absvalsq2d  10069  absge0d  10070  absval2d  10071  absnegd  10075  abscjd  10076  releabsd  10077  maxleim  10091  maxleast  10099  rexico  10107  maxclpr  10108  fimaxre2  10109  negfi  10110  minmax  10112  clim  10120  clim2  10122  climi  10126  climi2  10127  climi0  10128  climconst  10129  climmpt  10139  2clim  10140  climshftlemg  10141  climshft2  10145  climabs0  10146  subcn2  10150  cn1lem  10152  recn2  10155  imcn2  10156  climcn1lem  10157  climrecl  10162  climge0  10163  climadd  10164  climmul  10165  climsub  10166  climaddc2  10168  clim2iser  10175  clim2iser2  10176  iiserex  10177  iserige0  10181  climub  10182  climserile  10183  climcau  10184  climcvg1nlem  10186  climcaucn  10188  serif0  10189  sumeq1  10192  moddvds  10204  dvds1lem  10206  dvds2lem  10207  summodnegmod  10226  modmulconst  10227  dvds2ln  10228  dvdslelemd  10243  dvdsabseq  10247  divconjdvds  10249  dvdsdivcl  10250  dvdsssfz1  10252  dvds1  10253  alzdvds  10254  dvdsext  10255  fzo0dvdseq  10257  fzocongeq  10258  addmodlteqALT  10259  dvdsfac  10260  dvdsmod  10262  mulmoddvds  10263  zeo3  10267  zeo4  10269  odd2np1lem  10271  odd2np1  10272  oexpneg  10276  oddnn02np1  10280  oddge22np1  10281  2tp1odd  10284  zob  10291  ltoddhalfle  10293  opoe  10295  opeo  10297  omeo  10298  nn0ehalf  10303  nno  10306  nn0ob  10308  nn0oddm1d2  10309  nnoddm1d2  10310  divalglemnqt  10320  divalgmod  10327  flodddiv4  10334  flodddiv4t2lthalf  10337  zsupcllemstep  10341  infssuzex  10345  infssuzcldc  10347  dvdsbnd  10348  gcdsupex  10349  gcdsupcl  10350  gcdval  10351  gcddvds  10355  dvdslegcd  10356  gcdcl  10358  gcd2n0cl  10361  divgcdz  10363  divgcdnn  10366  gcdn0gt0  10369  gcd0id  10370  nn0gcdid0  10372  gcdneg  10373  gcdaddm  10375  gcdadd  10376  gcdid  10377  gcd1  10378  bezoutlemnewy  10385  bezoutlemstep  10386  bezoutlemmain  10387  bezoutlema  10388  bezoutlemb  10389  bezoutlemmo  10395  bezoutlemeu  10396  bezoutlemle  10397  bezoutlemsup  10398  dfgcd3  10399  dfgcd2  10403  absmulgcd  10406  gcdmultiple  10409  gcdmultiplez  10410  gcdzeq  10411  dvdssq  10420  bezoutr1  10422  ialgr0  10426  ialginv  10429  ialgcvg  10430  algcvgblem  10431  algcvgb  10432  ialgcvga  10433  eucalglt  10439  eucialgcvga  10440  eucialg  10441  lcmval  10445  dvdslcm  10451  lcmcl  10454  lcmneg  10456  lcmgcdlem  10459  lcmgcd  10460  lcmdvds  10461  lcmid  10462  lcmgcdeq  10465  coprmgcdb  10470  ncoprmgcdne1b  10471  ncoprmgcdgt1b  10472  mulgcddvds  10476  rpmulgcd2  10477  rpmul  10480  rpdvds  10481  divgcdcoprm0  10483  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  1nprm  10496  1idssfct  10497  isprm2lem  10498  isprm3  10500  isprm4  10501  prmind2  10502  dvdsprime  10504  dvdsnprmd  10507  3prm  10510  prmgt1  10513  prmm2nn0  10514  oddprmgt2  10515  sqnprm  10517  dvdsprm  10518  exprmfct  10519  prmdvdsfz  10520  nprmdvds1  10521  divgcdodd  10522  coprm  10523  euclemma  10525  isprm6  10526  rpexp  10532  sqrt2irrlem  10540  sqrt2irr  10541  pw2dvdslemn  10543  pw2dvdseulemle  10545  oddpwdclemxy  10547  oddpwdclemdvds  10548  oddpwdclemndvds  10549  oddpwdclemodd  10550  oddpwdclemdc  10551  oddpwdc  10552  sqpweven  10553  2sqpwodd  10554  sqrt2irraplemnn  10557  sqrt2irrap  10558  elabgft1  10588  bj-rspgt  10596  bj-nalset  10686  bj-inex  10698  bj-sels  10705  bj-unexg  10712  bj-notbid  10718  bj-indind  10727  speano5  10739  findset  10740  bj-bdfindisg  10743  bj-nn0suc  10759  bj-inf2vnlem1  10765  bj-inf2vn  10769  bj-inf2vn2  10770  bj-findis  10774  bj-findisg  10775