ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl Structured version   Unicode 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  pm5.21nii  619  ord  642  orcoms  648  orcd  651  orcs  653  biortn  663  pm4.67dc  780  annimim  781  imordc  795  pm4.54dc  804  pm4.55dc  845  dn1dc  866  dedlem0a  874  oplem1  881  simp1d  915  simp2d  916  simp3d  917  3adant1  921  3adant2  922  3adant3  923  3mix1d  1078  3mix2d  1079  3mix3d  1080  syl12anc  1132  syl21anc  1133  syl3anc  1134  syl3an1  1167  syl3an  1176  ecased  1238  xornbi  1274  pm5.15dc  1277  anxordi  1288  mpisyl  1332  a7s  1340  al2imi  1344  alimdh  1353  alrimih  1355  alcoms  1362  hbal  1363  albidh  1366  alequcoms  1406  nalequcoms  1407  nfrd  1410  sps  1427  hbor  1435  19.21bi  1447  nford  1456  nfand  1457  hbimd  1462  19.23bi  1480  exbi  1492  eximdh  1499  exbidh  1502  19.29  1508  19.29r2  1510  19.29x  1511  19.35-1  1512  19.25  1514  19.40-2  1520  i19.24  1527  i19.39  1528  alexim  1533  exanaliim  1535  hbnt  1540  hbnd  1542  nfnd  1544  19.9d  1548  19.36i  1559  19.41h  1572  ax9o  1585  equcoms  1591  ax10  1602  hbae  1603  hbaes  1605  hbnaes  1608  naecoms  1609  equs4  1610  equsexd  1614  spimt  1621  spimh  1622  cbv1h  1630  cbv2  1632  equvini  1638  equveli  1639  nfald  1640  nfexd  1641  stdpc4  1655  sbh  1656  equs5e  1673  ax10oe  1675  sb4a  1679  equs45f  1680  sb6f  1681  sb4e  1683  hbsb2a  1684  hbsb2e  1685  hbsb3  1686  ax16  1691  dveeq2  1693  ax11v2  1698  equs5or  1708  sbequi  1717  spsbe  1720  spsbim  1721  sbbid  1723  sbidm  1728  ax16i  1735  sbi2v  1769  cbvexdh  1798  nfsbt  1847  sbalyz  1872  dvelimdf  1889  sbal2  1895  mo23  1938  mor  1939  modc  1940  eu2  1941  mo3h  1950  euor2  1955  moexexdc  1981  2eu2ex  1986  bamalip  2018  bm1.1  2022  eqeq1d  2045  eqeq2d  2048  eleq1d  2103  eleq2d  2104  nfcrd  2188  dcned  2209  neeq1d  2218  neeq2d  2219  neleq12d  2297  ral2imi  2379  rexim  2407  reximdai  2411  r19.12  2416  rexlimd2  2425  r19.29  2444  r19.29d2r  2449  r19.29vva  2450  r19.35-1  2454  r19.36av  2455  raleqdv  2505  rexeqdv  2506  rabeqbidv  2546  rabeqbidva  2547  cgsexg  2583  cgsex2g  2584  cgsex4g  2585  vtoclgft  2598  vtoclgf  2606  vtocleg  2618  spcgft  2624  spcegft  2626  spc3gv  2639  rspct  2643  rspc2ev  2658  eqvincg  2662  pm13.183  2675  dedhb  2704  eueq3dc  2709  mosubt  2712  mob  2717  morex  2719  euind  2722  reuind  2738  sbceq1d  2763  sbcco2  2780  sbceqal  2808  sbcabel  2833  spesbcd  2838  rmo2i  2842  csbeq1d  2852  csbvarg  2871  sbcnestgf  2891  csbidmg  2896  csbco3g  2898  sseldi  2937  sseld  2938  sseq1d  2966  sseq2d  2967  uniiunlem  3022  psseq1d  3030  psseq2d  3031  pssssd  3035  pssned  3036  difeq1d  3055  difeq2d  3056  difss2d  3067  ssdifd  3073  sscond  3074  ssdifssd  3075  uneq1d  3090  uneq2d  3091  ineq1d  3131  ineq2d  3132  uneqin  3182  reuss2  3211  reupick2  3217  eq0rdv  3255  ssdisj  3271  ssnelpssd  3284  uneqdifeqim  3302  ralm  3319  iftrued  3332  iffalsed  3335  ifeq1d  3339  ifeq2d  3340  ifbid  3343  pweqd  3356  elpwid  3361  sneqd  3380  elpr2  3386  rabsnt  3436  preq1d  3444  preq2d  3445  tpeq1d  3450  tpeq2d  3451  tpeq3d  3452  snnzg  3476  snmg  3477  prmg  3480  snssd  3500  opeq1d  3546  opeq2d  3547  oteq1d  3552  oteq2d  3553  oteq3d  3554  opprc1  3562  opprc2  3563  oprcl  3564  unieqd  3582  unissd  3595  inteqd  3611  intmin3  3633  intmin4  3634  intab  3635  ss2iun  3663  iineq2  3665  iineq2d  3668  iuneq2dv  3669  iuneq1d  3671  dfiin2g  3681  ssiun  3690  iinss  3699  riinm  3720  disjss2  3739  disjeq2  3740  disjeq2dv  3741  disjss1  3742  disjeq1  3743  disjeq1d  3744  invdisj  3750  breq1d  3765  breqd  3766  breq2d  3767  mpteq1d  3833  triun  3858  trint  3860  repizf  3864  a9evsep  3870  nalset  3878  elssabg  3893  inteximm  3894  iinexgm  3899  pwne  3904  class2seteq  3907  bnd2  3917  abssexg  3925  snexgOLD  3926  snexg  3927  prelpwi  3941  rext  3942  pwel  3945  exss  3954  opexg  3955  opexgOLD  3956  opm  3962  opth1  3964  opth  3965  copsex2t  3973  copsex2g  3974  0nelop  3976  moop2  3979  opelopabsb  3988  ssopab2dv  4006  pwssunim  4012  poeq2  4028  sotritric  4052  sotritrieq  4053  sess1  4059  sess2  4060  seeq1  4061  seeq2  4062  onelss  4090  ordtr1  4091  ontr1  4092  limuni2  4100  trsuc  4125  tpexg  4145  eusvnf  4151  eusvnfb  4152  ralxfr2d  4162  rexxfr2d  4163  ralxfrALT  4165  reuhypd  4169  eldifpw  4174  op1stbg  4176  iunpw  4177  ssorduni  4179  ssonuni  4180  onun2  4182  onss  4185  orduni  4187  bm2.5ii  4188  ordsucim  4192  suceloni  4193  sucelon  4195  ordsucss  4196  onsucsssucr  4200  sucunielr  4201  ordtriexmidlem  4208  ordtri2orexmid  4211  onsucsssucexmid  4212  ordsucunielexmid  4216  regexmidlem1  4218  elirr  4224  en2lp  4232  opthreg  4234  ordsoexmid  4240  ordsuc  4241  ordpwsucss  4243  onnmin  4244  tfi  4248  tfisi  4253  peano2  4261  peano5  4264  findes  4269  nnord  4277  peano2b  4280  nn0eln0  4284  xpeq1d  4311  xpeq2d  4312  otelxp1  4322  mosubopt  4348  releqd  4367  relssdv  4375  xpsspw  4393  xpiindim  4416  relop  4429  ideqg  4430  coeq1d  4440  coeq2d  4441  cnveqd  4454  dmeqd  4480  rneqd  4506  rnss  4507  dmiin  4523  elrnmptg  4529  riinint  4536  dmrnssfld  4538  dmcosseq  4546  dmcoeq  4547  reseq1d  4554  reseq2d  4555  ssres2  4581  imaeq1d  4610  imaeq2d  4611  imasng  4633  elreimasng  4634  iniseg  4640  imass1  4643  imass2  4644  issref  4650  poirr2  4660  xpsndisj  4692  xpima1  4710  xpimasn  4712  opswapg  4750  elxp4  4751  elxp5  4752  relcoi1  4792  cnviinm  4802  iotaval  4821  iotanul  4825  iota4  4828  iota4an  4829  iotabidv  4831  iota2df  4834  funmo  4860  funss  4863  funeq  4864  funeqd  4866  funeu  4869  funco  4883  funun  4887  funcnvsn  4888  funprg  4892  funtpg  4893  fntpg  4898  fununi  4910  funcnvuni  4911  fun11uni  4912  funcnvres2  4917  imadiflem  4921  funimaexglem  4925  fneq1d  4932  fneq2d  4933  fnrel  4940  fneu  4946  fnco  4950  fnresdm  4951  2elresin  4953  fnssresb  4954  feq1d  4977  feq2d  4978  feq123d  4980  ffun  4991  frel  4992  fdm  4993  fco2  5000  fssxp  5001  ffdm  5004  fresin  5011  fcoi1  5013  fcoi2  5014  dmfex  5022  f00  5024  fnconstg  5027  f1fn  5036  f1fun  5037  f1rel  5038  f1dm  5039  f1ssres  5042  fofun  5050  fofn  5051  foima  5054  f1eq123d  5064  foeq123d  5065  f1oeq123d  5066  f1of  5069  f1ofn  5070  f1ofun  5071  f1orel  5072  f1odm  5073  f1ores  5084  f1orescnv  5085  f1imacnv  5086  foimacnv  5087  fun11iun  5090  resdif  5091  f1cnv  5093  fococnv2  5095  f1ococnv2  5096  f1cocnv2  5097  f1ococnv1  5098  f1cocnv1  5099  f1o00  5104  fo00  5105  f1osng  5110  brprcneu  5114  fvprc  5115  fveq1d  5123  fveq2d  5125  fvssunirng  5133  relfvssunirn  5134  funfvex  5135  fvexg  5137  sefvex  5139  relelfvdm  5148  nfvres  5149  nfunsn  5150  fnbrfvb  5157  funbrfv2b  5161  fvelrnb  5164  feqmptd  5169  fniinfv  5174  ssimaex  5177  funfvdm  5179  fvun1  5182  dmfco  5184  fvco2  5185  fvmptssdm  5198  fvmptdf  5201  fvmptdv2  5203  mpteqb  5204  eqfnfv  5208  fvreseq  5214  fndmdif  5215  fndmin  5217  chfnrn  5221  fvimacnvi  5224  fvimacnv  5225  fniniseg  5230  fniniseg2  5232  inpreima  5236  difpreima  5237  respreima  5238  fvelrn  5241  elrnrexdm  5249  ralrnmpt  5252  rexrnmpt  5253  dff3im  5255  dffo3  5257  dffo4  5258  dffo5  5259  fmpt  5262  f1ompt  5263  fmpt2d  5270  f1oresrab  5272  fmptco  5273  fmptcof  5274  fcompt  5276  fsn  5278  fsng  5279  fsn2  5280  dfmptg  5285  ressnop0  5287  fprg  5289  ftpg  5290  fressnfv  5293  fvconst  5294  fmptap  5296  fmptpr  5298  fvunsng  5300  fsnunf  5305  fsnunfv  5306  fconst3m  5323  resfunexg  5325  eufnfv  5332  fniunfv  5344  elunirn  5348  fnunirn  5349  dff13  5350  f1mpt  5353  f1ocnvfv2  5361  f1ocnvdm  5364  fcof1  5366  cbvfo  5368  cbvexfo  5369  cocan1  5370  fcof1o  5372  foeqcnvco  5373  f1eqcocnv  5374  fliftrel  5375  fliftel  5376  fliftfun  5379  fliftf  5382  isocnv  5394  isocnv2  5395  isores1  5397  isoini  5400  isoini2  5401  isopolem  5404  isopo  5405  isosolem  5406  isoso  5407  f1oiso  5408  riotass2  5437  riotass  5438  eusvobj1  5442  f1ofveu  5443  acexmidlemab  5449  acexmidlemcase  5450  acexmidlem1  5451  acexmidlem2  5452  oveq1d  5470  oveq2d  5471  oveqd  5472  ovprc1  5483  ovprc2  5484  brabvv  5493  ssoprab2  5503  fnoprabg  5544  mpt22eqb  5552  ralrnmpt2  5557  rexrnmpt2  5558  ovmpt2dxf  5568  ovmpt2df  5574  ovi3  5579  ovg  5581  ovres  5582  ovconst2  5594  f1ocnvd  5644  f1ocnv2d  5646  f1opw2  5648  f1opw  5649  suppssfv  5650  suppssov1  5651  offval  5661  ofrfval  5662  ofrval  5664  off  5666  offval2  5668  ofrfval2  5669  suppssof1  5670  ofco  5671  offveqb  5672  caofref  5674  caofinvl  5675  caofrss  5677  caoftrn  5678  cofunexg  5680  cofunex2g  5681  fnexALT  5682  fornex  5684  f1dmex  5685  abrexexg  5687  iunexg  5688  oprabexd  5696  offres  5704  ofmresex  5706  1stexg  5736  2ndexg  5737  op1steq  5747  1st2nd  5749  1stdm  5750  releldm2  5753  sbcopeq1a  5755  csbopeq1a  5756  dfoprab3  5759  eloprabi  5764  mpt2fvex  5771  mpt2exg  5776  fmpt2co  5779  1stconst  5784  2ndconst  5785  f2ndf  5789  fo2ndf  5790  f1o2ndf1  5791  mpt2xopn0yelv  5795  tposss  5802  tposeq  5803  tposeqd  5804  brtpos2  5807  brtposg  5810  tposexg  5814  dftpos4  5819  tposfo2  5823  tposf2  5824  tposf12  5825  2pwuninelg  5839  iunon  5840  issmo2  5845  smoeq  5846  smores  5848  smores2  5850  smodm2  5851  smoiso  5858  tfrlem1  5864  tfrlem5  5871  tfrlem6  5873  tfrlem8  5875  tfrlem9  5876  tfr0  5878  tfrlemisucaccv  5880  tfrlemibfn  5883  tfrlemiubacc  5885  tfrlemiex  5886  tfrexlem  5889  tfri2d  5891  tfri3  5894  rdgeq1  5898  rdgeq2  5899  rdgtfr  5901  rdgruledefgg  5902  rdgivallem  5908  rdgss  5910  rdgisuc1  5911  freceq1  5919  freceq2  5920  frec0g  5922  frectfr  5924  frecfnom  5925  frecsuclem1  5926  frecsuclemdm  5927  frecsuclem2  5928  frecsuclem3  5929  frecrdg  5931  freccl  5932  2oconcl  5961  sucinc2  5965  omfnex  5968  omv  5974  oeiv  5975  oeicl  5981  oav2  5982  oasuc  5983  oa1suc  5986  oawordi  5988  nna0  5992  nnm0  5993  nnacom  6002  nnaass  6003  nndi  6004  nnmass  6005  nnmsucr  6006  nnsucelsuc  6009  nnsucsssuc  6010  nntri3or  6011  nntri1  6013  nndceq  6015  nndcel  6016  nnaordi  6017  nnaord  6018  nnaword  6020  nnaordex  6036  nnm00  6038  ecexr  6047  ercl  6053  ersym  6054  ertr  6057  erref  6062  erssxp  6065  iserd  6068  brdifun  6069  swoer  6070  swoord1  6071  eceq1d  6078  ecss  6083  ereldm  6085  erth  6086  ecelqsg  6095  ecopqsi  6097  uniqs  6100  uniqs2  6102  elqsn0  6111  xpiderm  6113  iinerm  6114  riinerm  6115  ecinxp  6117  ecoptocl  6129  erovlem  6134  eroprf  6135  ecopovsym  6138  ecopover  6140  ecopovsymg  6141  ecopoverg  6143  th3qlem2  6145  th3q  6147  bren  6164  brdomg  6165  brdomi  6166  domrefg  6183  dom3d  6190  ener  6195  ensymd  6199  domtr  6201  f1imaen2g  6209  en0  6211  en1  6215  en1bg  6216  en1uniel  6220  2dom  6221  fundmen  6222  enm  6230  xpsnen  6231  xpcomco  6236  xpdom2  6241  xpdom3m  6244  fopwdom  6246  ssfiexmid  6254  pion  6294  piord  6295  elni2  6298  addpiord  6300  mulpiord  6301  mulidpi  6302  ltsopi  6304  mulclpi  6312  addnidpig  6320  indpi  6326  dfplpq2  6338  addcmpblnq  6351  mulcmpblnq  6352  dmaddpqlem  6361  nqpi  6362  dmaddpq  6363  dmmulpq  6364  mulcanenq  6369  distrnqg  6371  recexnq  6374  ltdcnq  6381  ltexnqq  6391  halfnq  6394  nsmallnqq  6395  nsmallnq  6396  subhalfnqq  6397  archnqq  6400  prarloclemarch  6401  prarloclemarch2  6402  ltrnqg  6403  ltrnqi  6404  nnnq  6405  ltnnnq  6406  enq0sym  6415  enq0ref  6416  enq0tr  6417  nqnq0pi  6421  nqnq0  6424  nq0nn  6425  addcmpblnq0  6426  mulcmpblnq0  6427  mulcanenq0ec  6428  addnq0mo  6430  mulnq0mo  6431  addnnnq0  6432  mulnnnq0  6433  nqpnq0nq  6436  nqnq0a  6437  nqnq0m  6438  nq0m0r  6439  nq0a0  6440  distrnq0  6442  addassnq0  6445  nq02m  6448  preqlu  6455  elinp  6457  prop  6458  prnmaddl  6473  prarloclemlt  6476  prarloclemlo  6477  prarloclem3  6480  prarloclemn  6482  prarloclem5  6483  prarloclemcalc  6485  prarloc  6486  genpml  6500  genpmu  6501  genprndl  6504  genprndu  6505  genpdisj  6506  genpassl  6507  genpassu  6508  addnqprllem  6510  addnqprulem  6511  addnqprl  6512  addnqpru  6513  addlocprlemlt  6514  addlocprlemeqgt  6515  addlocprlemeq  6516  addlocprlemgt  6517  addlocprlem  6518  nqprm  6525  nqprloc  6528  nnprlu  6534  addnqprlemrl  6538  addnqprlemru  6539  addnqprlemfl  6540  addnqprlemfu  6541  addnqpr  6542  appdivnq  6544  appdiv0nq  6545  prmuloclemcalc  6546  mulnqprl  6549  mulnqpru  6550  mullocprlem  6551  mullocpr  6552  ltprordil  6565  1idprl  6566  1idpru  6567  ltaddpr  6571  ltexprlemm  6574  ltexprlemlol  6576  ltexprlemopu  6577  ltexprlemupu  6578  ltexprlemdisj  6580  ltexprlemloc  6581  ltexprlemfl  6583  ltexprlemrl  6584  ltexprlemfu  6585  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  recexprlemell  6594  recexprlemelu  6595  recexprlemm  6596  recexprlemdisj  6602  recexprlemloc  6603  recexprlem1ssl  6605  recexprlem1ssu  6606  recexprlemss1l  6607  recexprlemss1u  6608  aptiprlemu  6612  ltmprr  6614  archpr  6615  cauappcvgprlemcan  6616  cauappcvgprlemm  6617  cauappcvgprlemdisj  6623  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlemladd  6630  cauappcvgprlem1  6631  cauappcvgprlem2  6632  archrecnq  6635  caucvgprlemk  6636  caucvgprlemm  6639  caucvgprlemloc  6646  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlem1  6650  caucvgprlem2  6651  addcmpblnr  6667  addsrmo  6671  mulsrmo  6672  addsrpr  6673  mulsrpr  6674  recexgt0sr  6701  recexsrlem  6702  addgt0sr  6703  archsr  6708  elreal2  6728  mulresr  6735  addcnsrec  6739  mulcnsrec  6740  pitonnlem2  6743  pitonn  6744  axaddcl  6750  axmulcl  6752  axrnegex  6763  mulid1  6822  mulid1d  6842  mulid2d  6843  recnd  6851  renepnfd  6873  renemnfd  6874  xrlenlt  6881  ltxrlt  6882  ltnrd  6926  readdcan  6950  addid1d  6959  addid2d  6960  cnegexlem3  6985  cnegex  6986  addcan  6988  addcan2  6989  subval  7000  negeqd  7003  subcl  7007  negcld  7105  subidd  7106  subid1d  7107  negidd  7108  negnegd  7109  negeq0d  7110  negrebd  7117  renegcld  7174  mul02lem2  7181  mul02d  7185  mul01d  7186  mulm1d  7203  lt0ne0d  7300  leidd  7301  lt0neg1d  7302  lt0neg2d  7303  le0neg1d  7304  le0neg2d  7305  recexre  7362  msqge0d  7402  mulge0  7403  recexap  7416  muleqadd  7431  divvalap  7435  divclap  7439  eqnegd  7491  div1d  7538  recgt1i  7645  recp1lt1  7646  recreclt  7647  ledivp1  7650  ltp1d  7677  lep1d  7678  ltm1d  7679  lem1d  7680  creur  7692  creui  7693  cju  7694  peano5nni  7698  peano2nn  7707  peano2nnd  7710  nn1suc  7714  nnge1  7718  nnrecgt0  7732  nnge1d  7737  nngt0d  7738  nnne0d  7739  nnrecred  7740  halfpos  7933  halfaddsubcl  7935  lt2halves  7937  nominpos  7939  avglt1  7940  avglt2  7941  avgle1  7942  avgle2  7943  2timesd  7944  times2d  7945  halfcld  7946  2halvesd  7947  rehalfcld  7948  nnrecl  7955  bndndx  7956  nnm1nn0  7999  elnnnn0c  8003  nn0supp  8010  nn0ge0d  8014  nn0ge2m1nn  8018  elnn0z  8034  elnnz1  8044  nn0negz  8055  peano2zm  8059  ztri3or  8064  zltp1le  8074  nn0n0n1ge2  8087  zdceq  8092  zdcle  8093  zdclt  8094  nn0n0n1ge2b  8096  nn0lt10b  8097  nn0ge0div  8103  zdiv  8104  recnz  8109  btwnnz  8110  zneo  8115  nneoor  8116  nneo  8117  zeo  8119  zeo2  8120  peano5uzti  8122  uzind2  8126  nn0ind-raph  8131  zindd  8132  btwnz  8133  znegcld  8138  peano2zd  8139  uzn0  8264  uzss  8269  eluzp1m1  8272  eluzaddi  8275  eluzsubi  8276  eluzadd  8277  eluzsub  8278  uzin  8281  peano2uzr  8304  uzind4  8307  elnn1uz2  8320  indstr2  8322  ublbneg  8324  negm  8326  lbzbi  8327  nn01to3  8328  nn0ge2m1nnALT  8329  divfnzn  8332  qapne  8350  rpne0  8373  difrp  8394  nnrpd  8396  rpgt0d  8400  rpge0d  8401  rpne0d  8402  rpreccld  8407  rphalfcld  8409  reclt1d  8410  recgt1d  8411  xrltnsym  8484  xrlttr  8486  xrltso  8487  xrlttri3  8488  nltpnft  8500  ngtmnft  8501  rexneg  8513  xnegneg  8516  xltnegi  8518  xnegcld  8525  ixxdisj  8542  eliooord  8567  elioc2  8575  elico2  8576  elicc2  8577  icodisj  8630  ioodisj  8631  iccf1o  8642  elfzel2  8658  elfzel1  8659  elfzelz  8660  elfzle1  8661  elfzle2  8662  elfzle3  8664  eluzfz1  8665  eluzfz2  8666  elfz3  8668  elfzubelfz  8670  fzm  8672  fzsplit2  8684  fzsplit  8685  fz01en  8687  elfz1end  8689  fznn0sub  8690  fzmmmeqm  8691  fzopth  8694  fzsuc  8701  fzpred  8702  elfzp1  8704  fzp1elp1  8707  fznatpl1  8708  fzpr  8709  fztp  8710  fzsuc2  8711  fzp1disj  8712  fzdifsuc  8713  fztpval  8715  fzrev3i  8720  elfz1b  8722  uzdisj  8725  fseq1p1m1  8726  fseq1m1p1  8727  fzm1  8732  fzneuz  8733  fznuz  8734  fzrevral  8737  fzshftral  8740  ige2m1fz  8742  elfz0add  8749  elfz0addOLD  8750  elfz0fzfz0  8753  uzsubfz0  8756  elfzmlbm  8758  elfzmlbmOLD  8759  elfzmlbp  8760  difelfznle  8763  nn0split  8764  nn0disj  8765  2ffzeq  8768  elfzo3  8789  fzonnsub2  8796  fzoss2  8798  fzossrbm1  8799  fzosplit  8803  fzo1fzo0n0  8809  fzonmapblen  8813  fzofzim  8814  fzocatel  8825  ubmelfzo  8826  elfzodifsumelfzo  8827  elfzom1elp1fzo  8828  fzval3  8830  zpnn0elfzo  8833  fzosplitsnm1  8835  fzossfzop1  8838  fzo0sn0fzo1  8847  fzoend  8848  ssfzo12  8850  ssfzo12bi  8851  ubmelm1fzo  8852  fzofzp1  8853  fzofzp1b  8854  elfzom1b  8855  peano2fzor  8858  fzosplitsn  8859  fzosplitprm1  8860  fzisfzounsn  8862  fzostep1  8863  fzoshftral  8864  frec2uz0d  8866  frec2uzsucd  8868  frec2uzuzd  8869  frec2uzrand  8872  frec2uzf1od  8873  frecuzrdgrrn  8875  frec2uzrdg  8876  frecuzrdgrom  8877  frecuzrdgfn  8879  frecuzrdgcl  8880  frecuzrdg0  8881  frecuzrdgsuc  8882  uzenom  8883  frecfzennn  8884  fzfig  8887  iseqeq1  8894  iseqeq2  8895  iseqeq4  8897  iseqovex  8899  iseqval  8900  iseqfn  8901  iseq1  8902  iseqcl  8903  iseqp1  8904  iseqfveq2  8905  iseqfeq2  8906  iseqfveq  8907  expival  8911  expnegap0  8917  expcllem  8920  qexpclz  8930  m1expcl2  8931  1exp  8938  expge0  8945  expge1  8946  expgt1  8947  mulexp  8948  exprecap  8950  expaddzaplem  8952  expaddzap  8953  expmul  8954  leexp2r  8962  exple1  8964  expubnd  8965  sqneg  8967  sqsubswap  8968  sqdivap  8972  sqgt0ap  8975  nnsqcl  8976  qsqcl  8978  sq11  8979  sqge0  8983  zsqcl2  8984  sumsqeq0  8985  sq0id  8999  nnlesq  9009  subsq2  9012  binom2  9015  binom3  9019  zesq  9020  nnesq  9021  bernneq  9022  bernneq3  9024  expnbnd  9025  exp0d  9028  exp1d  9029  sqvald  9031  sqcld  9032  0expd  9050  nnsqcld  9054  resqcld  9059  sqge0d  9060  cjval  9073  cjth  9074  cjf  9075  imval  9078  reim  9080  imcl  9082  crre  9085  crim  9086  replim  9087  remim  9088  reim0  9089  mulreap  9092  rere  9093  remullem  9099  redivap  9102  imdivap  9109  cjcj  9111  cjadd  9112  cjmulrcl  9115  cjmulval  9116  cjneg  9118  addcj  9119  cjexp  9121  imval2  9122  cjreim2  9132  cjdivap  9137  recld  9166  imcld  9167  cjcld  9168  replimd  9169  remimd  9170  cjcjd  9171  reim0bd  9172  rerebd  9173  cjrebd  9174  cjne0d  9175  recjd  9176  imcjd  9177  cjmulrcld  9178  cjmulvald  9179  cjmulge0d  9180  renegd  9181  imnegd  9182  cjnegd  9183  addcjd  9184  rered  9196  reim0d  9197  cjred  9198  rennim  9211  sqrt0rlem  9212  sqrtsq  9214  absneg  9219  abscj  9220  abs00bd  9224  absid  9225  absnid  9227  absre  9228  elabgft1  9252  bj-rspgt  9260  bj-nalset  9346  bj-inex  9358  bj-sels  9365  bj-unexg  9372  bj-notbid  9378  peano5set  9394  speano5  9398  findset  9399  bj-bdfindisg  9402  bj-nn0suc  9414  bj-inf2vnlem1  9420  bj-inf2vn  9424  bj-inf2vn2  9425  bj-findis  9429  bj-findisg  9430
  Copyright terms: Public domain W3C validator