ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl GIF version

Theorem syl 14
Description: An inference version of the transitive laws for implication imim2 49 and imim1 70, 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 (𝜑𝜓)
syl.2 (𝜓𝜒)
Assertion
Ref Expression
syl (𝜑𝜒)

Proof of Theorem syl
StepHypRef Expression
1 syl.1 . 2 (𝜑𝜓)
2 syl.2 . . 3 (𝜓𝜒)
32a1i 9 . 2 (𝜑 → (𝜓𝜒))
41, 3mpd 13 1 (𝜑𝜒)
Colors of variables: wff set class
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  23  sylcom  25  syl2im  34  sylsyld  52  pm2.86i  92  simpld  105  simprd  107  sylbi  114  sylbir  125  sylib  127  biimpd  132  sylibr  137  biantrud  288  biantrurd  289  pm2.01d  548  pm2.21d  549  pm2.24d  552  notnotd  560  pm5.21nii  620  ord  643  orcoms  649  orcd  652  orcs  654  biortn  664  pm4.67dc  781  annimim  782  imordc  796  pm4.54dc  805  pm4.55dc  846  dn1dc  867  dedlem0a  875  oplem1  882  simp1d  916  simp2d  917  simp3d  918  3adant1  922  3adant2  923  3adant3  924  3mix1d  1079  3mix2d  1080  3mix3d  1081  syl12anc  1133  syl21anc  1134  syl3anc  1135  syl3an1  1168  syl3an  1177  ecased  1239  xornbi  1277  pm5.15dc  1280  anxordi  1291  mpisyl  1335  a7s  1343  al2imi  1347  alimdh  1356  alrimih  1358  alcoms  1365  hbal  1366  albidh  1369  alequcoms  1409  nalequcoms  1410  nfrd  1413  sps  1430  hbor  1438  19.21bi  1450  nford  1459  nfand  1460  hbimd  1465  19.23bi  1483  exbi  1495  eximdh  1502  exbidh  1505  19.29  1511  19.29r2  1513  19.29x  1514  19.35-1  1515  19.25  1517  19.40-2  1523  i19.24  1530  i19.39  1531  alexim  1536  exanaliim  1538  hbnt  1543  hbnd  1545  nfnd  1547  19.9d  1551  19.36i  1562  19.41h  1575  ax9o  1588  equcoms  1594  ax10  1605  hbae  1606  hbaes  1608  hbnaes  1611  naecoms  1612  equs4  1613  equsexd  1617  spimt  1624  spimh  1625  cbv1h  1633  cbv2  1635  equvini  1641  equveli  1642  nfald  1643  nfexd  1644  stdpc4  1658  sbh  1659  equs5e  1676  ax10oe  1678  sb4a  1682  equs45f  1683  sb6f  1684  sb4e  1686  hbsb2a  1687  hbsb2e  1688  hbsb3  1689  ax16  1694  dveeq2  1696  ax11v2  1701  equs5or  1711  sbequi  1720  spsbe  1723  spsbim  1724  sbbid  1726  sbidm  1731  ax16i  1738  sbi2v  1772  cbvexdh  1801  nfsbt  1850  sbalyz  1875  dvelimdf  1892  sbal2  1898  mo23  1941  mor  1942  modc  1943  eu2  1944  mo3h  1953  euor2  1958  moexexdc  1984  2eu2ex  1989  bamalip  2021  bm1.1  2025  eqeq1d  2048  eqeq2d  2051  eleq1d  2106  eleq2d  2107  nfcrd  2191  dcned  2212  neeq1d  2223  neeq2d  2224  neleq12d  2303  ral2imi  2385  rexim  2413  reximdai  2417  r19.12  2422  rexlimd2  2431  r19.29  2450  r19.29d2r  2455  r19.29vva  2456  r19.35-1  2460  r19.36av  2461  raleqdv  2511  rexeqdv  2512  rabeqbidv  2552  rabeqbidva  2553  cgsexg  2589  cgsex2g  2590  cgsex4g  2591  vtoclgft  2604  vtoclgf  2612  vtocleg  2624  spcgft  2630  spcegft  2632  spc3gv  2645  rspct  2649  rspc2ev  2664  eqvincg  2668  pm13.183  2681  dedhb  2710  eueq3dc  2715  mosubt  2718  mob  2723  morex  2725  euind  2728  reuind  2744  sbceq1d  2769  sbcco2  2786  sbceqal  2814  sbcabel  2839  spesbcd  2844  rmo2i  2848  csbeq1d  2858  csbvarg  2877  sbcnestgf  2897  csbidmg  2902  csbco3g  2904  sseldi  2943  sseld  2944  sseq1d  2972  sseq2d  2973  uniiunlem  3028  psseq1d  3036  psseq2d  3037  pssssd  3041  pssned  3042  difeq1d  3061  difeq2d  3062  difss2d  3073  ssdifd  3079  sscond  3080  ssdifssd  3081  uneq1d  3096  uneq2d  3097  ineq1d  3137  ineq2d  3138  uneqin  3188  reuss2  3217  reupick2  3223  eq0rdv  3261  ssdisj  3277  ssnelpssd  3290  uneqdifeqim  3308  ralm  3325  iftrued  3338  iffalsed  3341  ifeq1d  3345  ifeq2d  3346  ifbid  3349  ifbothdc  3357  pweqd  3364  elpwid  3369  sneqd  3388  elpr2  3397  rabsnt  3445  preq1d  3453  preq2d  3454  tpeq1d  3459  tpeq2d  3460  tpeq3d  3461  snnzg  3485  snmg  3486  prmg  3489  snssd  3509  opeq1d  3555  opeq2d  3556  oteq1d  3561  oteq2d  3562  oteq3d  3563  opprc1  3571  opprc2  3572  oprcl  3573  unieqd  3591  unissd  3604  inteqd  3620  intmin3  3642  intmin4  3643  intab  3644  ss2iun  3672  iineq2  3674  iineq2d  3677  iuneq2dv  3678  iuneq1d  3680  dfiin2g  3690  ssiun  3699  iinss  3708  riinm  3729  disjss2  3748  disjeq2  3749  disjeq2dv  3750  disjss1  3751  disjeq1  3752  disjeq1d  3753  invdisj  3759  breq1d  3774  breqd  3775  breq2d  3776  mpteq1d  3842  triun  3867  trint  3869  repizf  3873  a9evsep  3879  nalset  3887  elssabg  3902  inteximm  3903  iinexgm  3908  pwne  3913  class2seteq  3916  bnd2  3926  abssexg  3934  snexgOLD  3935  snexg  3936  prelpwi  3950  rext  3951  pwel  3954  exss  3963  opexg  3964  opexgOLD  3965  opm  3971  opth1  3973  opth  3974  copsex2t  3982  copsex2g  3983  0nelop  3985  moop2  3988  opelopabsb  3997  ssopab2dv  4015  pwssunim  4021  poeq2  4037  sotritric  4061  sotritrieq  4062  sess1  4074  sess2  4075  seeq1  4076  seeq2  4077  frirrg  4087  onelss  4124  ordtr1  4125  ontr1  4126  limuni2  4134  trsuc  4159  tpexg  4179  eusvnf  4185  eusvnfb  4186  ralxfr2d  4196  rexxfr2d  4197  ralxfrALT  4199  reuhypd  4203  eldifpw  4208  op1stbg  4210  iunpw  4211  ssorduni  4213  ssonuni  4214  onun2  4216  onss  4219  orduni  4221  bm2.5ii  4222  ordsucim  4226  suceloni  4227  sucelon  4229  ordsucss  4230  onsucsssucr  4235  sucunielr  4236  onintonm  4243  ordtriexmidlem  4245  ordtri2orexmid  4248  ordtri2or2exmidlem  4251  onsucsssucexmid  4252  ordsucunielexmid  4256  regexmidlem1  4258  reg2exmidlema  4259  elirr  4266  ordn2lp  4269  en2lp  4278  opthreg  4280  ordsoexmid  4286  ordsuc  4287  onsucuni2  4288  ordpwsucss  4291  onnmin  4292  onintexmid  4297  ordwe  4300  wetriext  4301  wessep  4302  reg3exmidlemwe  4303  tfi  4305  tfisi  4310  peano2  4318  peano5  4321  findes  4326  nnord  4334  peano2b  4337  nn0eln0  4341  xpeq1d  4368  xpeq2d  4369  otelxp1  4379  mosubopt  4405  releqd  4424  relssdv  4432  xpsspw  4450  xpiindim  4473  relop  4486  ideqg  4487  coeq1d  4497  coeq2d  4498  cnveqd  4511  dmeqd  4537  rneqd  4563  rnss  4564  dmiin  4580  elrnmptg  4586  riinint  4593  dmrnssfld  4595  dmcosseq  4603  dmcoeq  4604  reseq1d  4611  reseq2d  4612  ssres2  4638  imaeq1d  4667  imaeq2d  4668  imasng  4690  elreimasng  4691  iniseg  4697  imass1  4700  imass2  4701  issref  4707  poirr2  4717  xpsndisj  4749  xpima1  4767  xpimasn  4769  opswapg  4807  elxp4  4808  elxp5  4809  relcoi1  4849  cnviinm  4859  iotaval  4878  iotanul  4882  iota4  4885  iota4an  4886  iotabidv  4888  iota2df  4891  funmo  4917  funss  4920  funeq  4921  funeqd  4923  funeu  4926  funco  4940  funun  4944  funcnvsn  4945  funprg  4949  funtpg  4950  fntpg  4955  fununi  4967  funcnvuni  4968  fun11uni  4969  funcnvres2  4974  imadiflem  4978  funimaexglem  4982  fneq1d  4989  fneq2d  4990  fnrel  4997  fneu  5003  fnco  5007  fnresdm  5008  2elresin  5010  fnssresb  5011  feq1d  5034  feq2d  5035  feq123d  5037  ffun  5048  frel  5049  fdm  5050  fco2  5057  fssxp  5058  ffdm  5061  fresin  5068  fcoi1  5070  fcoi2  5071  dmfex  5079  f00  5081  fnconstg  5084  f1fn  5093  f1fun  5094  f1rel  5095  f1dm  5096  f1ssres  5099  fofun  5107  fofn  5108  foima  5111  f1eq123d  5121  foeq123d  5122  f1oeq123d  5123  f1of  5126  f1ofn  5127  f1ofun  5128  f1orel  5129  f1odm  5130  f1ores  5141  f1orescnv  5142  f1imacnv  5143  foimacnv  5144  fun11iun  5147  resdif  5148  f1cnv  5150  fococnv2  5152  f1ococnv2  5153  f1cocnv2  5154  f1ococnv1  5155  f1cocnv1  5156  f1o00  5161  fo00  5162  f1osng  5167  brprcneu  5171  fvprc  5172  fveq1d  5180  fveq2d  5182  fvssunirng  5190  relfvssunirn  5191  funfvex  5192  fvexg  5194  sefvex  5196  relelfvdm  5205  nfvres  5206  nfunsn  5207  fnbrfvb  5214  funbrfv2b  5218  fvelrnb  5221  feqmptd  5226  fniinfv  5231  ssimaex  5234  funfvdm  5236  fvun1  5239  dmfco  5241  fvco2  5242  fvmptssdm  5255  fvmptdf  5258  fvmptdv2  5260  mpteqb  5261  eqfnfv  5265  fvreseq  5271  fndmdif  5272  fndmin  5274  chfnrn  5278  fvimacnvi  5281  fvimacnv  5282  fniniseg  5287  fniniseg2  5289  inpreima  5293  difpreima  5294  respreima  5295  fvelrn  5298  elrnrexdm  5306  ralrnmpt  5309  rexrnmpt  5310  dff3im  5312  dffo3  5314  dffo4  5315  dffo5  5316  fmpt  5319  f1ompt  5320  fmpt2d  5327  f1oresrab  5329  fmptco  5330  fmptcof  5331  fcompt  5333  fsn  5335  fsng  5336  fsn2  5337  dfmptg  5342  ressnop0  5344  fprg  5346  ftpg  5347  fressnfv  5350  fvconst  5351  fmptap  5353  fmptpr  5355  fvunsng  5357  fsnunf  5362  fsnunfv  5363  fconst3m  5380  resfunexg  5382  eufnfv  5389  fniunfv  5401  elunirn  5405  fnunirn  5406  dff13  5407  f1mpt  5410  f1ocnvfv2  5418  f1ocnvdm  5421  fcof1  5423  cbvfo  5425  cbvexfo  5426  cocan1  5427  fcof1o  5429  foeqcnvco  5430  f1eqcocnv  5431  fliftrel  5432  fliftel  5433  fliftfun  5436  fliftf  5439  isocnv  5451  isocnv2  5452  isores1  5454  isoini  5457  isoini2  5458  isopolem  5461  isopo  5462  isosolem  5463  isoso  5464  f1oiso  5465  riotass2  5494  riotass  5495  eusvobj1  5499  f1ofveu  5500  acexmidlemab  5506  acexmidlemcase  5507  acexmidlem1  5508  acexmidlem2  5509  oveq1d  5527  oveq2d  5528  oveqd  5529  ovprc1  5541  ovprc2  5542  brabvv  5551  ssoprab2  5561  fnoprabg  5602  mpt22eqb  5610  ralrnmpt2  5615  rexrnmpt2  5616  ovmpt2dxf  5626  ovmpt2df  5632  ovi3  5637  ovg  5639  ovres  5640  ovconst2  5652  f1ocnvd  5702  f1ocnv2d  5704  f1opw2  5706  f1opw  5707  suppssfv  5708  suppssov1  5709  offval  5719  ofrfval  5720  ofrval  5722  off  5724  offval2  5726  ofrfval2  5727  suppssof1  5728  ofco  5729  offveqb  5730  caofref  5732  caofinvl  5733  caofrss  5735  caoftrn  5736  cofunexg  5738  cofunex2g  5739  fnexALT  5740  fornex  5742  f1dmex  5743  abrexexg  5745  iunexg  5746  oprabexd  5754  offres  5762  ofmresex  5764  1stexg  5794  2ndexg  5795  op1steq  5805  1st2nd  5807  1stdm  5808  releldm2  5811  sbcopeq1a  5813  csbopeq1a  5814  dfoprab3  5817  eloprabi  5822  mpt2fvex  5829  mpt2exg  5834  fmpt2co  5837  1stconst  5842  2ndconst  5843  f2ndf  5847  fo2ndf  5848  f1o2ndf1  5849  mpt2xopn0yelv  5854  tposss  5861  tposeq  5862  tposeqd  5863  brtpos2  5866  brtposg  5869  tposexg  5873  dftpos4  5878  tposfo2  5882  tposf2  5883  tposf12  5884  2pwuninelg  5898  iunon  5899  issmo2  5904  smoeq  5905  smores  5907  smores2  5909  smodm2  5910  smoiso  5917  tfrlem1  5923  tfrlem5  5930  tfrlem6  5932  tfrlem8  5934  tfrlem9  5935  tfr0  5937  tfrlemisucaccv  5939  tfrlemibfn  5942  tfrlemiubacc  5944  tfrlemiex  5945  tfrexlem  5948  tfri2d  5950  tfri3  5953  rdgeq1  5958  rdgeq2  5959  rdgtfr  5961  rdgruledefgg  5962  rdgivallem  5968  rdgss  5970  rdgisuc1  5971  freceq1  5979  freceq2  5980  frec0g  5983  frectfr  5985  frecfnom  5986  frecsuclem1  5987  frecsuclemdm  5988  frecsuclem2  5989  frecsuclem3  5990  frecrdg  5992  freccl  5993  2oconcl  6022  sucinc2  6026  omfnex  6029  omv  6035  oeiv  6036  oeicl  6042  oav2  6043  oasuc  6044  oa1suc  6047  oawordi  6049  nna0  6053  nnm0  6054  nnacom  6063  nnaass  6064  nndi  6065  nnmass  6066  nnmsucr  6067  nnsucelsuc  6070  nnsucsssuc  6071  nntri3or  6072  nntri1  6074  nntri2or2  6076  nndceq  6077  nndcel  6078  nnsseleq  6079  nndifsnid  6080  nnaordi  6081  nnaord  6082  nnaword  6084  nnaordex  6100  nnm00  6102  ecexr  6111  ercl  6117  ersym  6118  ertr  6121  erref  6126  erssxp  6129  iserd  6132  brdifun  6133  swoer  6134  swoord1  6135  eceq1d  6142  ecss  6147  ereldm  6149  erth  6150  ecelqsg  6159  ecopqsi  6161  uniqs  6164  uniqs2  6166  elqsn0  6175  xpiderm  6177  iinerm  6178  riinerm  6179  ecinxp  6181  ecoptocl  6193  erovlem  6198  eroprf  6199  ecopovsym  6202  ecopover  6204  ecopovsymg  6205  ecopoverg  6207  th3qlem2  6209  th3q  6211  bren  6228  brdomg  6229  brdomi  6230  domrefg  6247  dom3d  6254  ener  6259  ensymd  6263  domtr  6265  f1imaen2g  6273  en0  6275  en1  6279  en1bg  6280  en1uniel  6284  2dom  6285  fundmen  6286  enm  6294  xpsnen  6295  xpcomco  6300  xpdom2  6305  xpdom3m  6308  fopwdom  6310  phplem1  6315  phplem2  6316  phplem3  6317  phplem4  6318  phplem4dom  6324  nndomo  6326  phpm  6327  phpelm  6328  phplem4on  6329  fidceq  6330  fidifsnen  6331  fidifsnid  6332  ssfiexmid  6336  dif1en  6337  php5fin  6339  fin0  6342  fin0or  6343  diffitest  6344  findcard2  6346  findcard2s  6347  ac6sfi  6352  nnwetri  6354  onunsnss  6355  ordiso2  6357  isnumi  6362  oncardval  6366  carden2bex  6369  pion  6408  piord  6409  elni2  6412  addpiord  6414  mulpiord  6415  mulidpi  6416  ltsopi  6418  mulclpi  6426  addnidpig  6434  indpi  6440  dfplpq2  6452  addcmpblnq  6465  mulcmpblnq  6466  dmaddpqlem  6475  nqpi  6476  dmaddpq  6477  dmmulpq  6478  mulcanenq  6483  distrnqg  6485  recexnq  6488  ltdcnq  6495  ltexnqq  6506  halfnq  6509  nsmallnqq  6510  nsmallnq  6511  subhalfnqq  6512  archnqq  6515  prarloclemarch  6516  prarloclemarch2  6517  ltrnqg  6518  ltrnqi  6519  nnnq  6520  ltnnnq  6521  enq0sym  6530  enq0ref  6531  enq0tr  6532  nqnq0pi  6536  nqnq0  6539  nq0nn  6540  addcmpblnq0  6541  mulcmpblnq0  6542  mulcanenq0ec  6543  addnq0mo  6545  mulnq0mo  6546  addnnnq0  6547  mulnnnq0  6548  nqpnq0nq  6551  nqnq0a  6552  nqnq0m  6553  nq0m0r  6554  nq0a0  6555  distrnq0  6557  addassnq0  6560  nq02m  6563  preqlu  6570  elinp  6572  prop  6573  prnmaddl  6588  prarloclemlt  6591  prarloclemlo  6592  prarloclem3  6595  prarloclemn  6597  prarloclem5  6598  prarloclemcalc  6600  prarloc  6601  genpml  6615  genpmu  6616  genprndl  6619  genprndu  6620  genpdisj  6621  genpassl  6622  genpassu  6623  addnqprllem  6625  addnqprulem  6626  addnqprl  6627  addnqpru  6628  addlocprlemlt  6629  addlocprlemeqgt  6630  addlocprlemeq  6631  addlocprlemgt  6632  addlocprlem  6633  nqprm  6640  nqprloc  6643  nnprlu  6651  addnqprlemrl  6655  addnqprlemru  6656  addnqprlemfl  6657  addnqprlemfu  6658  addnqpr  6659  appdivnq  6661  appdiv0nq  6662  prmuloclemcalc  6663  mulnqprl  6666  mulnqpru  6667  mullocprlem  6668  mullocpr  6669  mulnqprlemrl  6671  mulnqprlemru  6672  mulnqprlemfl  6673  mulnqprlemfu  6674  mulnqpr  6675  ltprordil  6687  1idprl  6688  1idpru  6689  ltnqpri  6692  ltaddpr  6695  ltexprlemm  6698  ltexprlemlol  6700  ltexprlemopu  6701  ltexprlemupu  6702  ltexprlemdisj  6704  ltexprlemloc  6705  ltexprlemfl  6707  ltexprlemrl  6708  ltexprlemfu  6709  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  lteupri  6715  prplnqu  6718  recexprlemell  6720  recexprlemelu  6721  recexprlemm  6722  recexprlemdisj  6728  recexprlemloc  6729  recexprlem1ssl  6731  recexprlem1ssu  6732  recexprlemss1l  6733  recexprlemss1u  6734  aptiprlemu  6738  ltmprr  6740  archpr  6741  caucvgprlemcanl  6742  cauappcvgprlemm  6743  cauappcvgprlemdisj  6749  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlemladd  6756  cauappcvgprlem1  6757  cauappcvgprlem2  6758  archrecnq  6761  archrecpr  6762  caucvgprlemk  6763  caucvgprlemm  6766  caucvgprlemloc  6773  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlem1  6777  caucvgprlem2  6778  caucvgprprlemloccalc  6782  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemnjltk  6789  caucvgprprlemnbj  6791  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemupu  6798  caucvgprprlemloc  6801  caucvgprprlemexbt  6804  caucvgprprlemexb  6805  caucvgprprlemaddq  6806  caucvgprprlem1  6807  caucvgprprlem2  6808  addcmpblnr  6824  addsrmo  6828  mulsrmo  6829  addsrpr  6830  mulsrpr  6831  recexgt0sr  6858  recexsrlem  6859  addgt0sr  6860  archsr  6866  srpospr  6867  prsrriota  6872  caucvgsrlemcl  6873  caucvgsrlemasr  6874  caucvgsrlemcau  6877  caucvgsrlemgt1  6879  caucvgsrlemoffval  6880  caucvgsrlemoffres  6884  caucvgsr  6886  elreal2  6907  mulresr  6914  addcnsrec  6918  mulcnsrec  6919  pitonnlem2  6923  pitonn  6924  pitore  6926  recnnre  6927  peano2nnnn  6929  ltrennb  6930  recidpipr  6932  recidpirqlemcalc  6933  recidpirq  6934  axaddcl  6940  axmulcl  6942  axrnegex  6953  rereceu  6963  recriota  6964  peano5nnnn  6966  nntopi  6968  axcaucvglemcl  6969  axcaucvglemcau  6972  axcaucvglemres  6973  mulid1  7024  mulid1d  7044  mulid2d  7045  recnd  7054  renepnfd  7076  renemnfd  7077  xrlenlt  7084  ltxrlt  7085  ltnrd  7129  readdcan  7153  addid1d  7162  addid2d  7163  cnegexlem3  7188  cnegex  7189  addcan  7191  addcan2  7192  subval  7203  negeqd  7206  subcl  7210  negcld  7309  subidd  7310  subid1d  7311  negidd  7312  negnegd  7313  negeq0d  7314  negrebd  7321  renegcld  7378  mul02lem2  7385  mul02d  7389  mul01d  7390  mulm1d  7407  lt0ne0d  7505  leidd  7506  lt0neg1d  7507  lt0neg2d  7508  le0neg1d  7509  le0neg2d  7510  recexre  7569  msqge0d  7609  mulge0  7610  leltap  7615  ap0gt0  7629  recexap  7634  muleqadd  7649  divvalap  7653  divclap  7657  eqnegd  7709  div1d  7756  recgt1i  7864  recp1lt1  7865  recreclt  7866  ledivp1  7869  ltp1d  7896  lep1d  7897  ltm1d  7898  lem1d  7899  creur  7911  creui  7912  cju  7913  peano5nni  7917  peano2nn  7926  peano2nnd  7929  nn1suc  7933  nnge1  7937  nnrecgt0  7951  nnge1d  7956  nngt0d  7957  nnne0d  7958  nnap0d  7959  nnrecred  7960  halfpos  8156  halfaddsubcl  8158  lt2halves  8160  nominpos  8162  avglt1  8163  avglt2  8164  avgle1  8165  avgle2  8166  2timesd  8167  times2d  8168  halfcld  8169  2halvesd  8170  rehalfcld  8171  div4p1lem1div2  8177  nnrecl  8179  bndndx  8180  nnm1nn0  8223  elnnnn0c  8227  nn0supp  8234  nn0ge0d  8238  nn0ge2m1nn  8242  elnn0z  8258  elnnz1  8268  nn0negz  8279  peano2zm  8283  ztri3or  8288  zltp1le  8298  nn0n0n1ge2  8311  zdceq  8316  zdcle  8317  zdclt  8318  nn0n0n1ge2b  8320  nn0lt10b  8321  nn0ge0div  8327  zdiv  8328  recnz  8333  btwnnz  8334  zneo  8339  nneoor  8340  nneo  8341  zeo  8343  zeo2  8344  peano5uzti  8346  uzind2  8350  nn0ind-raph  8355  zindd  8356  btwnz  8357  znegcld  8362  peano2zd  8363  uzn0  8488  uzss  8493  eluzp1m1  8496  eluzaddi  8499  eluzsubi  8500  eluzadd  8501  eluzsub  8502  uzin  8505  peano2uzr  8528  uzind4  8531  elnn1uz2  8544  indstr2  8546  ublbneg  8548  negm  8550  lbzbi  8551  nn01to3  8552  nn0ge2m1nnALT  8553  divfnzn  8556  qapne  8574  rpne0  8598  difrp  8619  nnrpd  8621  rpgt0d  8625  rpge0d  8626  rpne0d  8627  rpap0d  8628  rpreccld  8633  rphalfcld  8635  reclt1d  8636  recgt1d  8637  divge1  8649  ledivge1le  8652  xrltnsym  8714  xrlttr  8716  xrltso  8717  xrlttri3  8718  nltpnft  8730  ngtmnft  8731  rexneg  8743  xnegneg  8746  xltnegi  8748  xnegcld  8755  ixxdisj  8772  eliooord  8797  elioc2  8805  elico2  8806  elicc2  8807  icodisj  8860  ioodisj  8861  iccf1o  8872  elfzel2  8888  elfzel1  8889  elfzelz  8890  elfzle1  8891  elfzle2  8892  elfzle3  8894  eluzfz1  8895  eluzfz2  8896  elfz3  8898  elfzubelfz  8900  fzm  8902  fzsplit2  8914  fzsplit  8915  fz01en  8917  elfz1end  8919  fznn0sub  8920  fzmmmeqm  8921  fzopth  8924  fzsuc  8931  fzpred  8932  elfzp1  8934  fzp1elp1  8937  fznatpl1  8938  fzpr  8939  fztp  8940  fzsuc2  8941  fzp1disj  8942  fzdifsuc  8943  fztpval  8945  fzrev3i  8950  elfz1b  8952  uzdisj  8955  fseq1p1m1  8956  fseq1m1p1  8957  fzm1  8962  fzneuz  8963  fznuz  8964  fzrevral  8967  fzshftral  8970  ige2m1fz  8972  elfz0add  8979  elfz0addOLD  8980  elfz0fzfz0  8983  uzsubfz0  8986  elfzmlbm  8988  elfzmlbmOLD  8989  elfzmlbp  8990  difelfznle  8993  nn0split  8994  nn0disj  8995  2ffzeq  8998  elfzo3  9019  fzonnsub2  9026  fzoss2  9028  fzossrbm1  9029  fzosplit  9033  fzo1fzo0n0  9039  fzonmapblen  9043  fzofzim  9044  fzocatel  9055  ubmelfzo  9056  elfzodifsumelfzo  9057  elfzom1elp1fzo  9058  fzval3  9060  zpnn0elfzo  9063  fzosplitsnm1  9065  fzossfzop1  9068  fzo0sn0fzo1  9077  fzoend  9078  ssfzo12  9080  ssfzo12bi  9081  ubmelm1fzo  9082  fzofzp1  9083  fzofzp1b  9084  elfzom1b  9085  peano2fzor  9088  fzosplitsn  9089  fzosplitprm1  9090  fzisfzounsn  9092  fzostep1  9093  fzoshftral  9094  subfzo0  9097  qdceq  9102  qbtwnzlemex  9105  rebtwn2z  9109  qbtwnre  9111  flqcl  9117  flqlelt  9118  flqcld  9119  flqlt  9125  flid  9126  flqidm  9127  flqltnz  9129  flqwordi  9130  flqbi  9132  adddivflid  9134  flqmulnn0  9141  flhalf  9144  fldivnn0le  9145  flltdivnn0lt  9146  fldiv4p1lem1div2  9147  ceilqval  9148  ceiqge  9151  ceiqm1l  9153  ceiqle  9155  ceilid  9157  flqeqceilz  9160  intfracq  9162  flqdiv  9163  modqcl  9168  flqpmodeq  9169  modq0  9171  mulqmod0  9172  negqmod0  9173  modqge0  9174  modqlt  9175  modqelico  9176  zmod10  9182  modqmulnn  9184  frec2uz0d  9185  frec2uzsucd  9187  frec2uzuzd  9188  frec2uzrand  9191  frec2uzf1od  9192  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdgrom  9196  frecuzrdgfn  9198  frecuzrdgcl  9199  frecuzrdg0  9200  frecuzrdgsuc  9201  uzenom  9202  frecfzennn  9203  fzfig  9206  iseqeq1  9214  iseqeq2  9215  iseqeq4  9217  iseqovex  9219  iseqval  9220  iseqfn  9221  iseq1  9222  iseqcl  9223  iseqp1  9225  iseqm1  9227  iseqfveq2  9228  iseqfeq2  9229  iseqfveq  9230  iseqshft2  9232  monoord  9235  monoord2  9236  isermono  9237  iseqsplit  9238  iseq1p  9239  iseqcaopr3  9240  iseqid3  9245  iseqid3s  9246  iseqid  9247  iseqhomo  9248  serige0  9252  serile  9253  expival  9257  expnegap0  9263  expcllem  9266  qexpclz  9276  m1expcl2  9277  1exp  9284  expge0  9291  expge1  9292  expgt1  9293  mulexp  9294  exprecap  9296  expaddzaplem  9298  expaddzap  9299  expmul  9300  leexp2r  9308  exple1  9310  expubnd  9311  sqneg  9313  sqsubswap  9314  sqdivap  9318  sqgt0ap  9322  nnsqcl  9323  qsqcl  9325  sq11  9326  sqge0  9330  zsqcl2  9331  sumsqeq0  9332  sq0id  9346  nnlesq  9356  subsq2  9359  binom2  9362  binom3  9366  zesq  9367  nnesq  9368  bernneq  9369  bernneq3  9371  expnbnd  9372  exp0d  9375  exp1d  9376  sqvald  9378  sqcld  9379  0expd  9397  nnsqcld  9401  resqcld  9406  sqge0d  9407  shftlem  9417  shftfvalg  9419  shftfibg  9421  shftdm  9423  shftfib  9424  shftfn  9425  shftval  9426  2shfti  9432  cjval  9445  cjth  9446  cjf  9447  imval  9450  reim  9452  imcl  9454  crre  9457  crim  9458  replim  9459  remim  9460  reim0  9461  mulreap  9464  rere  9465  remullem  9471  redivap  9474  imdivap  9481  cjcj  9483  cjadd  9484  cjmulrcl  9487  cjmulval  9488  cjneg  9490  addcj  9491  cjexp  9493  imval2  9494  cjreim2  9504  cjdivap  9509  recld  9538  imcld  9539  cjcld  9540  replimd  9541  remimd  9542  cjcjd  9543  reim0bd  9544  rerebd  9545  cjrebd  9546  cjne0d  9547  cjap0d  9548  recjd  9549  imcjd  9550  cjmulrcld  9551  cjmulvald  9552  cjmulge0d  9553  renegd  9554  imnegd  9555  cjnegd  9556  addcjd  9557  rered  9569  reim0d  9570  cjred  9571  caucvgrelemcau  9579  caucvgre  9580  cvg1nlemres  9584  cvg1n  9585  r19.29uz  9590  recvguniq  9593  rennim  9600  sqrt0rlem  9601  resqrexlemover  9608  resqrexlemcalc3  9614  resqrexlemnm  9616  resqrexlemcvg  9617  resqrexlemgt0  9618  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemga  9621  resqrtcl  9627  sqrtsq  9642  absneg  9648  abscj  9650  sqabsadd  9653  sqabssub  9654  absrpclap  9659  abs00ad  9663  abs00bd  9664  absreimsq  9665  absreim  9666  absmul  9667  absdivap  9668  absid  9669  absnid  9671  leabs  9672  absre  9673  absresq  9674  absrele  9679  absimle  9680  ltabs  9683  abslt  9684  absle  9685  abssubap0  9686  lenegsq  9691  releabs  9692  recvalap  9693  nnabscl  9696  abssub  9697  abstri  9700  abs2dif  9702  abs2difabs  9704  abs3lem  9707  cau3lem  9710  cau4  9712  caubnd2  9713  rpsqrtcld  9754  leabsd  9757  absred  9758  abscld  9777  absvalsqd  9778  absvalsq2d  9779  absge0d  9780  absval2d  9781  absnegd  9785  abscjd  9786  releabsd  9787  clim  9802  clim2  9804  climi  9808  climi2  9809  climi0  9810  climconst  9811  climmpt  9821  2clim  9822  climshftlemg  9823  climshft2  9827  climabs0  9828  subcn2  9832  cn1lem  9834  recn2  9837  imcn2  9838  climcn1lem  9839  climrecl  9844  climge0  9845  climadd  9846  climmul  9847  climsub  9848  climaddc2  9850  clim2iser  9857  clim2iser2  9858  iiserex  9859  iserige0  9863  climub  9864  climserile  9865  climcau  9866  climcvg1nlem  9868  climcaucn  9870  serif0  9871  sumeq1  9874  sqr2irrlem  9877  sqrt2irr  9878  ialgr0  9883  ialginv  9886  ialgcvg  9887  algcvgblem  9888  algcvgb  9889  ialgcvga  9890  elabgft1  9917  bj-rspgt  9925  bj-nalset  10015  bj-inex  10027  bj-sels  10034  bj-unexg  10041  bj-notbid  10047  bj-indind  10056  peano5setOLD  10065  speano5  10069  findset  10070  bj-bdfindisg  10073  bj-nn0suc  10089  bj-inf2vnlem1  10095  bj-inf2vn  10099  bj-inf2vn2  10100  bj-findis  10104  bj-findisg  10105
  Copyright terms: Public domain W3C validator