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

Theorem syl 14
Description: An inference version of the transitive laws for implication imim2 53 and imim1 74, 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
StepHypRef Expression
1 syl.1 . 2  |-  ( ph  ->  ps )
2 syl.2 . . 3  |-  ( ps 
->  ch )
32a1i 9 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mpd 13 1  |-  ( ph  ->  ch )
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  26  sylcom  28  syl11  31  syl2im  38  sylsyld  56  pm2.86i  96  simpld  109  simprd  111  sylbi  118  sylbir  129  sylib  131  biimpd  136  sylibr  141  biantrud  292  biantrurd  293  pm2.01d  558  pm2.21d  559  pm2.24d  562  notnotd  570  pm5.21nii  630  ord  653  orcoms  659  orcd  662  orcs  664  biortn  674  pm4.67dc  792  annimim  793  imordc  807  pm4.54dc  816  pm4.55dc  857  dn1dc  878  dedlem0a  886  oplem1  893  simp1d  927  simp2d  928  simp3d  929  3adant1  933  3adant2  934  3adant3  935  3mix1d  1090  3mix2d  1091  3mix3d  1092  syl12anc  1144  syl21anc  1145  syl3anc  1146  syl3an1  1179  syl3an  1188  mp3an12i  1247  ecased  1255  xornbi  1293  pm5.15dc  1296  anxordi  1307  mpisyl  1351  a7s  1359  al2imi  1363  alimdh  1372  alrimih  1374  alcoms  1381  hbal  1382  albidh  1385  alequcoms  1425  nalequcoms  1426  nfrd  1429  sps  1446  hbor  1454  19.21bi  1466  nford  1475  nfand  1476  hbimd  1481  19.23bi  1499  exbi  1511  eximdh  1518  exbidh  1521  19.29  1527  19.29r2  1529  19.29x  1530  19.35-1  1531  19.25  1533  19.40-2  1539  i19.24  1546  i19.39  1547  alexim  1552  exanaliim  1554  hbnt  1559  hbnd  1561  nfnd  1563  19.9d  1567  19.36i  1578  19.41h  1591  ax9o  1604  equcoms  1610  ax10  1621  hbae  1622  hbaes  1624  hbnaes  1627  naecoms  1628  equs4  1629  equsexd  1633  spimt  1640  spimh  1641  cbv1h  1649  cbv2  1651  equvini  1657  equveli  1658  nfald  1659  nfexd  1660  stdpc4  1674  sbh  1675  equs5e  1692  ax10oe  1694  sb4a  1698  equs45f  1699  sb6f  1700  sb4e  1702  hbsb2a  1703  hbsb2e  1704  hbsb3  1705  ax16  1710  dveeq2  1712  ax11v2  1717  equs5or  1727  sbequi  1736  spsbe  1739  spsbim  1740  sbbid  1742  sbidm  1747  ax16i  1754  sbi2v  1788  cbvexdh  1817  nfsbt  1866  sbalyz  1891  dvelimdf  1908  sbal2  1914  mo23  1957  mor  1958  modc  1959  eu2  1960  mo3h  1969  euor2  1974  moexexdc  2000  2eu2ex  2005  bamalip  2037  bm1.1  2041  eqeq1d  2064  eqeq2d  2067  eleq1d  2122  eleq2d  2123  nfcrd  2207  dcned  2226  neeq1d  2238  neeq2d  2239  neleq12d  2320  ral2imi  2402  rexim  2430  reximdai  2434  r19.12  2439  rexlimd2  2448  r19.29  2467  r19.29d2r  2472  r19.29vva  2473  r19.35-1  2477  r19.36av  2478  raleqdv  2528  rexeqdv  2529  rabeqbidv  2569  rabeqbidva  2570  cgsexg  2606  cgsex2g  2607  cgsex4g  2608  vtoclgft  2621  vtoclgf  2629  vtocleg  2641  spcgft  2647  spcegft  2649  spc3gv  2662  rspct  2666  rspc2ev  2687  eqvincg  2691  pm13.183  2704  dedhb  2733  eueq3dc  2738  mosubt  2741  mob  2746  morex  2748  euind  2751  reuind  2767  sbceq1d  2792  sbcco2  2809  sbceqal  2841  sbcabel  2867  spesbcd  2872  rmo2i  2876  csbeq1d  2886  csbvarg  2905  sbcnestgf  2925  csbidmg  2930  csbco3g  2932  sseldi  2971  sseld  2972  sseq1d  3000  sseq2d  3001  uniiunlem  3056  psseq1d  3064  psseq2d  3065  pssssd  3069  pssned  3070  difeq1d  3089  difeq2d  3090  difss2d  3101  ssdifd  3107  sscond  3108  ssdifssd  3109  uneq1d  3124  uneq2d  3125  ineq1d  3165  ineq2d  3166  uneqin  3216  reuss2  3245  reupick2  3251  eq0rdv  3289  ssdisj  3305  ssnelpssd  3318  uneqdifeqim  3336  ralm  3353  iftrued  3366  iffalsed  3369  ifeq1d  3373  ifeq2d  3374  ifbid  3377  ifbothdc  3385  pweqd  3392  elpwid  3397  sneqd  3416  elpr2  3425  rabsnt  3473  preq1d  3481  preq2d  3482  tpeq1d  3487  tpeq2d  3488  tpeq3d  3489  snnzg  3513  snmg  3514  prmg  3517  snssd  3537  opeq1d  3583  opeq2d  3584  oteq1d  3589  oteq2d  3590  oteq3d  3591  opprc1  3599  opprc2  3600  oprcl  3601  unieqd  3619  unissd  3632  inteqd  3648  intmin3  3670  intmin4  3671  intab  3672  ss2iun  3700  iineq2  3702  iineq2d  3705  iuneq2dv  3706  iuneq1d  3708  dfiin2g  3718  ssiun  3727  iinss  3736  riinm  3757  disjss2  3776  disjeq2  3777  disjeq2dv  3778  disjss1  3779  disjeq1  3780  disjeq1d  3781  invdisj  3787  breq1d  3802  breqd  3803  breq2d  3804  mpteq1d  3870  triun  3895  trint  3897  repizf  3901  a9evsep  3907  nalset  3915  elssabg  3930  inteximm  3931  iinexgm  3936  pwne  3941  class2seteq  3944  bnd2  3954  abssexg  3962  snexgOLD  3963  snexg  3964  prelpwi  3978  rext  3979  pwel  3982  exss  3991  opexg  3992  opexgOLD  3993  opm  3999  opth1  4001  opth  4002  copsex2t  4010  copsex2g  4011  0nelop  4013  moop2  4016  opelopabsb  4025  ssopab2dv  4043  pwssunim  4049  poeq2  4065  sotritric  4089  sotritrieq  4090  sess1  4102  sess2  4103  seeq1  4104  seeq2  4105  frirrg  4115  onelss  4152  ordtr1  4153  ontr1  4154  limuni2  4162  trsuc  4187  tpexg  4207  eusvnf  4213  eusvnfb  4214  ralxfr2d  4224  rexxfr2d  4225  ralxfrALT  4227  reuhypd  4231  eldifpw  4236  op1stbg  4238  iunpw  4239  ssorduni  4241  ssonuni  4242  onun2  4244  onss  4247  orduni  4249  bm2.5ii  4250  ordsucim  4254  suceloni  4255  sucelon  4257  ordsucss  4258  onsucsssucr  4263  sucunielr  4264  onintonm  4271  ordtriexmidlem  4273  ordtri2orexmid  4276  ordtri2or2exmidlem  4279  onsucsssucexmid  4280  ordsucunielexmid  4284  regexmidlem1  4286  reg2exmidlema  4287  elirr  4294  ordn2lp  4297  en2lp  4306  opthreg  4308  ordsoexmid  4314  ordsuc  4315  onsucuni2  4316  ordpwsucss  4319  onnmin  4320  onintexmid  4325  ordwe  4328  wetriext  4329  wessep  4330  reg3exmidlemwe  4331  tfi  4333  tfisi  4338  peano2  4346  peano5  4349  findes  4354  nnord  4362  peano2b  4365  nn0eln0  4369  xpeq1d  4396  xpeq2d  4397  otelxp1  4407  mosubopt  4433  releqd  4452  relssdv  4460  xpsspw  4478  xpiindim  4501  relop  4514  ideqg  4515  coeq1d  4525  coeq2d  4526  cnveqd  4539  dmeqd  4565  rneqd  4591  rnss  4592  dmiin  4608  elrnmptg  4614  riinint  4621  dmrnssfld  4623  dmcosseq  4631  dmcoeq  4632  reseq1d  4639  reseq2d  4640  ssres2  4666  imaeq1d  4695  imaeq2d  4696  imasng  4718  elreimasng  4719  iniseg  4725  imass1  4728  imass2  4729  issref  4735  poirr2  4745  xpsndisj  4777  xpima1  4795  xpimasn  4797  opswapg  4835  elxp4  4836  elxp5  4837  relcoi1  4877  cnviinm  4887  iotaval  4906  iotanul  4910  iota4  4913  iota4an  4914  iotabidv  4916  iota2df  4919  funmo  4945  funss  4948  funeq  4949  funeqd  4951  funeu  4954  funco  4968  funun  4972  funcnvsn  4973  funprg  4977  funtpg  4978  fntpg  4983  fununi  4995  funcnvuni  4996  fun11uni  4997  funcnvres2  5002  imadiflem  5006  funimaexglem  5010  fneq1d  5017  fneq2d  5018  fnrel  5025  fneu  5031  fnco  5035  fnresdm  5036  2elresin  5038  fnssresb  5039  feq1d  5062  feq2d  5063  feq123d  5065  ffun  5076  frel  5077  fdm  5078  fco2  5085  fssxp  5086  ffdm  5089  fresin  5096  fcoi1  5098  fcoi2  5099  dmfex  5107  f00  5109  fnconstg  5112  f1fn  5121  f1fun  5122  f1rel  5123  f1dm  5124  f1ssres  5127  fofun  5135  fofn  5136  foima  5139  f1eq123d  5149  foeq123d  5150  f1oeq123d  5151  f1of  5154  f1ofn  5155  f1ofun  5156  f1orel  5157  f1odm  5158  f1ores  5169  f1orescnv  5170  f1imacnv  5171  foimacnv  5172  fun11iun  5175  resdif  5176  f1cnv  5178  fococnv2  5180  f1ococnv2  5181  f1cocnv2  5182  f1ococnv1  5183  f1cocnv1  5184  f1o00  5189  fo00  5190  f1osng  5195  brprcneu  5199  fvprc  5200  fveq1d  5208  fveq2d  5210  fvssunirng  5218  relfvssunirn  5219  funfvex  5220  fvexg  5222  sefvex  5224  relelfvdm  5233  nfvres  5234  nfunsn  5235  fnbrfvb  5242  funbrfv2b  5246  fvelrnb  5249  feqmptd  5254  fniinfv  5259  ssimaex  5262  funfvdm  5264  fvun1  5267  dmfco  5269  fvco2  5270  fvmptssdm  5283  fvmptdf  5286  fvmptdv2  5288  mpteqb  5289  eqfnfv  5293  fvreseq  5299  fndmdif  5300  fndmin  5302  chfnrn  5306  fvimacnvi  5309  fvimacnv  5310  fniniseg  5315  fniniseg2  5317  inpreima  5321  difpreima  5322  respreima  5323  fvelrn  5326  elrnrexdm  5334  ralrnmpt  5337  rexrnmpt  5338  dff3im  5340  dffo3  5342  dffo4  5343  dffo5  5344  fmpt  5347  f1ompt  5348  fmpt2d  5355  f1oresrab  5357  fmptco  5358  fmptcof  5359  fcompt  5361  fsn  5363  fsng  5364  fsn2  5365  dfmptg  5370  ressnop0  5372  fprg  5374  ftpg  5375  fressnfv  5378  fvconst  5379  fmptap  5381  fmptpr  5383  fvunsng  5385  fsnunf  5390  fsnunfv  5391  fconst3m  5408  resfunexg  5410  eufnfv  5417  fniunfv  5429  elunirn  5433  fnunirn  5434  dff13  5435  f1mpt  5438  f1ocnvfv2  5446  f1ocnvdm  5449  fcof1  5451  cbvfo  5453  cbvexfo  5454  cocan1  5455  fcof1o  5457  foeqcnvco  5458  f1eqcocnv  5459  fliftrel  5460  fliftel  5461  fliftfun  5464  fliftf  5467  isocnv  5479  isocnv2  5480  isores1  5482  isoini  5485  isoini2  5486  isopolem  5489  isopo  5490  isosolem  5491  isoso  5492  f1oiso  5493  riotass2  5522  riotass  5523  eusvobj1  5527  f1ofveu  5528  acexmidlemab  5534  acexmidlemcase  5535  acexmidlem1  5536  acexmidlem2  5537  oveq1d  5555  oveq2d  5556  oveqd  5557  ovprc1  5569  ovprc2  5570  brabvv  5579  ssoprab2  5589  fnoprabg  5630  mpt22eqb  5638  ralrnmpt2  5643  rexrnmpt2  5644  ovmpt2dxf  5654  ovmpt2df  5660  ovi3  5665  ovg  5667  ovres  5668  ovconst2  5680  f1ocnvd  5730  f1ocnv2d  5732  f1opw2  5734  f1opw  5735  suppssfv  5736  suppssov1  5737  offval  5747  ofrfval  5748  ofrval  5750  off  5752  offval2  5754  ofrfval2  5755  suppssof1  5756  ofco  5757  offveqb  5758  caofref  5760  caofinvl  5761  caofrss  5763  caoftrn  5764  cofunexg  5766  cofunex2g  5767  fnexALT  5768  fornex  5770  f1dmex  5771  abrexexg  5773  iunexg  5774  oprabexd  5782  offres  5790  ofmresex  5792  1stexg  5822  2ndexg  5823  op1steq  5833  1st2nd  5835  1stdm  5836  releldm2  5839  sbcopeq1a  5841  csbopeq1a  5842  dfoprab3  5845  eloprabi  5850  mpt2fvex  5857  mpt2exg  5862  fmpt2co  5865  1stconst  5870  2ndconst  5871  f2ndf  5875  fo2ndf  5876  f1o2ndf1  5877  cnvoprab  5883  f1od2  5884  mpt2xopn0yelv  5885  tposss  5892  tposeq  5893  tposeqd  5894  brtpos2  5897  brtposg  5900  tposexg  5904  dftpos4  5909  tposfo2  5913  tposf2  5914  tposf12  5915  2pwuninelg  5929  iunon  5930  issmo2  5935  smoeq  5936  smores  5938  smores2  5940  smodm2  5941  smoiso  5948  tfrlem1  5954  tfrlem5  5961  tfrlem6  5963  tfrlem8  5965  tfrlem9  5966  tfr0  5968  tfrlemisucaccv  5970  tfrlemibfn  5973  tfrlemiubacc  5975  tfrlemiex  5976  tfrexlem  5979  tfri2d  5981  tfri3  5984  rdgeq1  5989  rdgeq2  5990  rdgtfr  5992  rdgruledefgg  5993  rdgivallem  5999  rdgss  6001  rdgisuc1  6002  freceq1  6010  freceq2  6011  frec0g  6014  frectfr  6016  frecfnom  6017  frecsuclem1  6018  frecsuclemdm  6019  frecsuclem2  6020  frecsuclem3  6021  frecrdg  6023  freccl  6024  2oconcl  6053  sucinc2  6057  omfnex  6060  omv  6066  oeiv  6067  oeicl  6073  oav2  6074  oasuc  6075  oa1suc  6078  oawordi  6080  nna0  6084  nnm0  6085  nnacom  6094  nnaass  6095  nndi  6096  nnmass  6097  nnmsucr  6098  nnsucelsuc  6101  nnsucsssuc  6102  nntri3or  6103  nntri1  6105  nntri2or2  6107  nndceq  6108  nndcel  6109  nnsseleq  6110  nndifsnid  6111  nnaordi  6112  nnaord  6113  nnaword  6115  nnaordex  6131  nnm00  6133  ecexr  6142  ercl  6148  ersym  6149  ertr  6152  erref  6157  erssxp  6160  iserd  6163  brdifun  6164  swoer  6165  swoord1  6166  eceq1d  6173  ecss  6178  ereldm  6180  erth  6181  ecelqsg  6190  ecopqsi  6192  uniqs  6195  uniqs2  6197  elqsn0  6206  xpiderm  6208  iinerm  6209  riinerm  6210  ecinxp  6212  ecoptocl  6224  erovlem  6229  eroprf  6230  ecopovsym  6233  ecopover  6235  ecopovsymg  6236  ecopoverg  6238  th3qlem2  6240  th3q  6242  bren  6259  brdomg  6260  brdomi  6261  domrefg  6278  dom3d  6285  ener  6290  ensymd  6294  domtr  6296  f1imaen2g  6304  en0  6306  en1  6310  en1bg  6311  en1uniel  6315  2dom  6316  fundmen  6317  enm  6325  xpsnen  6326  xpcomco  6331  xpdom2  6336  xpdom3m  6339  fopwdom  6341  phplem1  6346  phplem2  6347  phplem3  6348  phplem4  6349  phplem4dom  6355  nndomo  6357  phpm  6358  phpelm  6359  phplem4on  6360  fidceq  6361  fidifsnen  6362  fidifsnid  6363  ssfiexmid  6367  dif1en  6368  php5fin  6370  fin0  6373  fin0or  6374  diffitest  6375  findcard2  6377  findcard2s  6378  ac6sfi  6383  nnwetri  6385  onunsnss  6386  supeq1d  6393  supval2ti  6401  supclti  6404  supubti  6405  suplubti  6406  supsnti  6409  isotilem  6410  isoti  6411  supisolem  6412  supisoex  6413  supisoti  6414  ordiso2  6415  isnumi  6420  oncardval  6424  carden2bex  6427  pion  6466  piord  6467  elni2  6470  addpiord  6472  mulpiord  6473  mulidpi  6474  ltsopi  6476  mulclpi  6484  addnidpig  6492  indpi  6498  dfplpq2  6510  addcmpblnq  6523  mulcmpblnq  6524  dmaddpqlem  6533  nqpi  6534  dmaddpq  6535  dmmulpq  6536  mulcanenq  6541  distrnqg  6543  recexnq  6546  ltdcnq  6553  ltexnqq  6564  halfnq  6567  nsmallnqq  6568  nsmallnq  6569  subhalfnqq  6570  archnqq  6573  prarloclemarch  6574  prarloclemarch2  6575  ltrnqg  6576  ltrnqi  6577  nnnq  6578  ltnnnq  6579  enq0sym  6588  enq0ref  6589  enq0tr  6590  nqnq0pi  6594  nqnq0  6597  nq0nn  6598  addcmpblnq0  6599  mulcmpblnq0  6600  mulcanenq0ec  6601  addnq0mo  6603  mulnq0mo  6604  addnnnq0  6605  mulnnnq0  6606  nqpnq0nq  6609  nqnq0a  6610  nqnq0m  6611  nq0m0r  6612  nq0a0  6613  distrnq0  6615  addassnq0  6618  nq02m  6621  preqlu  6628  elinp  6630  prop  6631  prnmaddl  6646  prarloclemlt  6649  prarloclemlo  6650  prarloclem3  6653  prarloclemn  6655  prarloclem5  6656  prarloclemcalc  6658  prarloc  6659  genpml  6673  genpmu  6674  genprndl  6677  genprndu  6678  genpdisj  6679  genpassl  6680  genpassu  6681  addnqprllem  6683  addnqprulem  6684  addnqprl  6685  addnqpru  6686  addlocprlemlt  6687  addlocprlemeqgt  6688  addlocprlemeq  6689  addlocprlemgt  6690  addlocprlem  6691  nqprm  6698  nqprloc  6701  nnprlu  6709  addnqprlemrl  6713  addnqprlemru  6714  addnqprlemfl  6715  addnqprlemfu  6716  addnqpr  6717  appdivnq  6719  appdiv0nq  6720  prmuloclemcalc  6721  mulnqprl  6724  mulnqpru  6725  mullocprlem  6726  mullocpr  6727  mulnqprlemrl  6729  mulnqprlemru  6730  mulnqprlemfl  6731  mulnqprlemfu  6732  mulnqpr  6733  ltprordil  6745  1idprl  6746  1idpru  6747  ltnqpri  6750  ltaddpr  6753  ltexprlemm  6756  ltexprlemlol  6758  ltexprlemopu  6759  ltexprlemupu  6760  ltexprlemdisj  6762  ltexprlemloc  6763  ltexprlemfl  6765  ltexprlemrl  6766  ltexprlemfu  6767  ltexprlemru  6768  addcanprleml  6770  addcanprlemu  6771  lteupri  6773  prplnqu  6776  recexprlemell  6778  recexprlemelu  6779  recexprlemm  6780  recexprlemdisj  6786  recexprlemloc  6787  recexprlem1ssl  6789  recexprlem1ssu  6790  recexprlemss1l  6791  recexprlemss1u  6792  aptiprlemu  6796  ltmprr  6798  archpr  6799  caucvgprlemcanl  6800  cauappcvgprlemm  6801  cauappcvgprlemdisj  6807  cauappcvgprlemladdfu  6810  cauappcvgprlemladdfl  6811  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  cauappcvgprlemladd  6814  cauappcvgprlem1  6815  cauappcvgprlem2  6816  archrecnq  6819  archrecpr  6820  caucvgprlemk  6821  caucvgprlemm  6824  caucvgprlemloc  6831  caucvgprlemladdfu  6833  caucvgprlemladdrl  6834  caucvgprlem1  6835  caucvgprlem2  6836  caucvgprprlemloccalc  6840  caucvgprprlemnkltj  6845  caucvgprprlemnkeqj  6846  caucvgprprlemnjltk  6847  caucvgprprlemnbj  6849  caucvgprprlemml  6850  caucvgprprlemmu  6851  caucvgprprlemopl  6853  caucvgprprlemlol  6854  caucvgprprlemopu  6855  caucvgprprlemupu  6856  caucvgprprlemloc  6859  caucvgprprlemexbt  6862  caucvgprprlemexb  6863  caucvgprprlemaddq  6864  caucvgprprlem1  6865  caucvgprprlem2  6866  addcmpblnr  6882  addsrmo  6886  mulsrmo  6887  addsrpr  6888  mulsrpr  6889  recexgt0sr  6916  recexsrlem  6917  addgt0sr  6918  archsr  6924  srpospr  6925  prsrriota  6930  caucvgsrlemcl  6931  caucvgsrlemasr  6932  caucvgsrlemcau  6935  caucvgsrlemgt1  6937  caucvgsrlemoffval  6938  caucvgsrlemoffres  6942  caucvgsr  6944  elreal2  6965  mulresr  6972  addcnsrec  6976  mulcnsrec  6977  pitonnlem2  6981  pitonn  6982  pitore  6984  recnnre  6985  peano2nnnn  6987  ltrennb  6988  recidpipr  6990  recidpirqlemcalc  6991  recidpirq  6992  axaddcl  6998  axmulcl  7000  axrnegex  7011  rereceu  7021  recriota  7022  peano5nnnn  7024  nntopi  7026  axcaucvglemcl  7027  axcaucvglemcau  7030  axcaucvglemres  7031  mulid1  7082  mulid1d  7102  mulid2d  7103  recnd  7113  renepnfd  7135  renemnfd  7136  xrlenlt  7143  ltxrlt  7144  ltnrd  7188  readdcan  7214  addid1d  7223  addid2d  7224  cnegexlem3  7251  cnegex  7252  addcan  7254  addcan2  7255  subval  7266  negeqd  7269  subcl  7273  negcld  7372  subidd  7373  subid1d  7374  negidd  7375  negnegd  7376  negeq0d  7377  negrebd  7384  renegcld  7450  mul02lem2  7457  mul02d  7461  mul01d  7462  mulm1d  7479  lt0ne0d  7579  leidd  7580  lt0neg1d  7581  lt0neg2d  7582  le0neg1d  7583  le0neg2d  7584  recexre  7643  msqge0d  7683  mulge0  7684  leltap  7689  ap0gt0  7703  recexap  7708  muleqadd  7723  divvalap  7727  divclap  7731  muldivdirap  7758  eqnegd  7784  div1d  7831  recgt1i  7939  recp1lt1  7940  recreclt  7941  ledivp1  7944  ltp1d  7971  lep1d  7972  ltm1d  7973  lem1d  7974  creur  7987  creui  7988  cju  7989  peano5nni  7993  peano2nn  8002  peano2nnd  8005  nn1suc  8009  nnge1  8013  nnrecgt0  8027  nnge1d  8032  nngt0d  8033  nnne0d  8034  nnap0d  8035  nnrecred  8036  halfpos  8213  halfaddsubcl  8215  lt2halves  8217  nominpos  8219  avglt1  8220  avglt2  8221  avgle1  8222  avgle2  8223  2timesd  8224  times2d  8225  halfcld  8226  2halvesd  8227  rehalfcld  8228  xp1d2m1eqxm1d2  8234  div4p1lem1div2  8235  nnrecl  8237  bndndx  8238  nnm1nn0  8280  elnnnn0c  8284  nn0supp  8291  nn0ge0d  8295  nn0ge2m1nn  8299  elnn0z  8315  elnnz1  8325  nn0negz  8336  peano2zm  8340  ztri3or  8345  zltp1le  8356  nn0n0n1ge2  8369  zdceq  8374  zdcle  8375  zdclt  8376  nn0n0n1ge2b  8378  nn0lt10b  8379  nn0ge0div  8385  zdiv  8386  recnz  8391  btwnnz  8392  zneo  8398  nneoor  8399  nneo  8400  zeo  8402  zeo2  8403  peano5uzti  8405  uzind2  8409  nn0ind-raph  8414  zindd  8415  btwnz  8416  znegcld  8421  peano2zd  8422  uzn0  8584  uzss  8589  eluzp1m1  8592  eluzaddi  8595  eluzsubi  8596  eluzadd  8597  eluzsub  8598  uzin  8601  peano2uzr  8624  uzind4  8627  elnn1uz2  8641  indstr2  8643  ublbneg  8645  negm  8647  lbzbi  8648  nn01to3  8649  nn0ge2m1nnALT  8650  divfnzn  8653  qapne  8671  rpne0  8696  difrp  8717  nnrpd  8719  rpgt0d  8723  rpge0d  8724  rpne0d  8725  rpap0d  8726  rpreccld  8731  rphalfcld  8733  reclt1d  8734  recgt1d  8735  divge1  8747  ledivge1le  8750  nn0ledivnn  8785  xrltnsym  8815  xrlttr  8817  xrltso  8818  xrlttri3  8819  nltpnft  8831  ngtmnft  8832  rexneg  8844  xnegneg  8847  xltnegi  8849  xnegcld  8856  ixxdisj  8873  eliooord  8898  elioc2  8906  elico2  8907  elicc2  8908  icodisj  8961  ioodisj  8962  iccf1o  8973  elfzel2  8990  elfzel1  8991  elfzelz  8992  elfzle1  8993  elfzle2  8994  elfzle3  8996  eluzfz1  8997  eluzfz2  8998  elfz3  9000  elfzubelfz  9002  fzm  9004  fzsplit2  9016  fzsplit  9017  fz01en  9019  elfz1end  9021  fznn0sub  9022  fzmmmeqm  9023  fzopth  9026  fzsuc  9033  fzpred  9034  elfzp1  9036  fzp1elp1  9039  fznatpl1  9040  fzpr  9041  fztp  9042  fzsuc2  9043  fzp1disj  9044  fzdifsuc  9045  fztpval  9047  fzrev3i  9052  elfz1b  9054  uzdisj  9057  fseq1p1m1  9058  fseq1m1p1  9059  fzm1  9064  fzneuz  9065  fznuz  9066  fzrevral  9069  fzshftral  9072  ige2m1fz  9074  elfz0add  9081  elfz0addOLD  9082  elfz0fzfz0  9085  uzsubfz0  9088  elfzmlbm  9090  elfzmlbmOLD  9091  elfzmlbp  9092  difelfznle  9095  nn0split  9096  nn0disj  9097  2ffzeq  9100  elfzo3  9121  fzonnsub2  9128  fzoss2  9130  fzossrbm1  9131  fzosplit  9135  fzo1fzo0n0  9141  fzonmapblen  9145  fzofzim  9146  fzocatel  9157  ubmelfzo  9158  elfzodifsumelfzo  9159  elfzom1elp1fzo  9160  fzval3  9162  zpnn0elfzo  9165  fzosplitsnm1  9167  fzossfzop1  9170  fzo0sn0fzo1  9179  fzoend  9180  ssfzo12  9182  ssfzo12bi  9183  ubmelm1fzo  9184  fzofzp1  9185  fzofzp1b  9186  elfzom1b  9187  peano2fzor  9190  fzosplitsn  9191  fzosplitprm1  9192  fzisfzounsn  9194  fzostep1  9195  fzoshftral  9196  subfzo0  9199  qdceq  9204  qbtwnzlemex  9207  rebtwn2z  9211  qbtwnre  9213  qbtwnxr  9214  ioo0  9216  ico0  9218  ioc0  9219  flqcl  9225  flqlelt  9226  flqcld  9227  flqlt  9233  flid  9234  flqidm  9235  flqltnz  9237  flqwordi  9238  flqbi  9240  adddivflid  9242  flqmulnn0  9249  flhalf  9252  fldivnn0le  9253  flltdivnn0lt  9254  fldiv4p1lem1div2  9255  ceilqval  9256  ceiqge  9259  ceiqm1l  9261  ceiqle  9263  ceilid  9265  flqeqceilz  9268  intfracq  9270  flqdiv  9271  modqcl  9276  flqpmodeq  9277  modq0  9279  mulqmod0  9280  negqmod0  9281  modqge0  9282  modqlt  9283  modqelico  9284  zmod10  9290  modqmulnn  9292  zmodfzo  9297  zmodid2  9302  zmodidfzo  9303  modqabs  9307  modqabs2  9308  modqcyc  9309  modqadd1  9311  modqaddabs  9312  mulp1mod1  9315  modqmuladd  9316  modqmuladdim  9317  modqmuladdnn0  9318  qnegmod  9319  m1modge3gt1  9321  addmodid  9322  modqadd2mod  9324  modqm1p1mod0  9325  modqltm1p1mod  9326  modqmul1  9327  modqmul12d  9328  modqnegd  9329  modqadd12d  9330  modqsub12d  9331  q2submod  9335  modifeq2int  9336  modaddmodup  9337  modaddmodlo  9338  modqmulmodr  9340  modqaddmulmod  9341  modqdi  9342  modqsubdir  9343  modqeqmodmin  9344  modfzo0difsn  9345  modsumfzodifsn  9346  addmodlteq  9348  frec2uz0d  9349  frec2uzsucd  9351  frec2uzuzd  9352  frec2uzrand  9355  frec2uzf1od  9356  frecuzrdgrrn  9358  frec2uzrdg  9359  frecuzrdgrom  9360  frecuzrdgfn  9362  frecuzrdgcl  9363  frecuzrdg0  9364  frecuzrdgsuc  9365  uzenom  9366  frecfzennn  9367  fzfig  9370  iseqeq1  9378  iseqeq2  9379  iseqeq4  9381  iseqovex  9383  iseqval  9384  iseqfn  9385  iseq1  9386  iseqcl  9387  iseqp1  9389  iseqm1  9391  iseqfveq2  9392  iseqfeq2  9393  iseqfveq  9394  iseqshft2  9396  monoord  9399  monoord2  9400  isermono  9401  iseqsplit  9402  iseq1p  9403  iseqcaopr3  9404  iseqid3  9409  iseqid3s  9410  iseqid  9411  iseqhomo  9412  iseqz  9413  serige0  9417  serile  9418  expival  9422  expnegap0  9428  expcllem  9431  qexpclz  9441  m1expcl2  9442  1exp  9449  expge0  9456  expge1  9457  expgt1  9458  mulexp  9459  exprecap  9461  expaddzaplem  9463  expaddzap  9464  expmul  9465  m1expeven  9467  leexp2r  9474  exple1  9476  expubnd  9477  sqneg  9479  sqsubswap  9480  sqdivap  9484  sqgt0ap  9488  nnsqcl  9489  qsqcl  9491  sq11  9492  sqge0  9496  zsqcl2  9497  sumsqeq0  9498  sq0id  9512  nnlesq  9522  iexpcyc  9523  subsq2  9526  binom2  9529  binom3  9534  zesq  9535  nnesq  9536  bernneq  9537  bernneq3  9539  expnbnd  9540  exp0d  9543  exp1d  9544  sqvald  9546  sqcld  9547  0expd  9565  sqoddm1div8  9569  nnsqcld  9570  resqcld  9575  sqge0d  9576  facnn  9595  fac0  9596  fac1  9597  facp1  9598  faccld  9604  facndiv  9607  facwordi  9608  faclbnd  9609  faclbnd6  9612  facavg  9614  bcval  9617  bcrpcl  9621  bccmpl  9622  bcn0  9623  bcn1  9626  bcnp1n  9627  bcm1k  9628  bcp1n  9629  bcp1nk  9630  ibcval5  9631  bcn2  9632  bcp1m1  9633  bcpasc  9634  bccl  9635  bcn2m1  9637  permnn  9639  shftlem  9645  shftfvalg  9647  shftfibg  9649  shftdm  9651  shftfib  9652  shftfn  9653  shftval  9654  2shfti  9660  cjval  9673  cjth  9674  cjf  9675  imval  9678  reim  9680  imcl  9682  crre  9685  crim  9686  replim  9687  remim  9688  reim0  9689  mulreap  9692  rere  9693  remullem  9699  redivap  9702  imdivap  9709  cjcj  9711  cjadd  9712  cjmulrcl  9715  cjmulval  9716  cjneg  9718  addcj  9719  cjexp  9721  imval2  9722  cjreim2  9732  cjdivap  9737  recld  9766  imcld  9767  cjcld  9768  replimd  9769  remimd  9770  cjcjd  9771  reim0bd  9772  rerebd  9773  cjrebd  9774  cjne0d  9775  cjap0d  9776  recjd  9777  imcjd  9778  cjmulrcld  9779  cjmulvald  9780  cjmulge0d  9781  renegd  9782  imnegd  9783  cjnegd  9784  addcjd  9785  rered  9797  reim0d  9798  cjred  9799  caucvgrelemcau  9807  caucvgre  9808  cvg1nlemres  9812  cvg1n  9813  r19.29uz  9819  recvguniq  9822  rennim  9829  sqrt0rlem  9830  resqrexlemover  9837  resqrexlemcalc3  9843  resqrexlemnm  9845  resqrexlemcvg  9846  resqrexlemgt0  9847  resqrexlemoverl  9848  resqrexlemglsq  9849  resqrexlemga  9850  resqrtcl  9856  sqrtsq  9871  absneg  9877  abscj  9879  sqabsadd  9882  sqabssub  9883  absrpclap  9888  abs00ad  9892  abs00bd  9893  absreimsq  9894  absreim  9895  absmul  9896  absdivap  9897  absid  9898  absnid  9900  leabs  9901  qabsord  9903  absre  9904  absresq  9905  absrele  9910  absimle  9911  ltabs  9914  abslt  9915  absle  9916  abssubap0  9917  lenegsq  9922  releabs  9923  recvalap  9924  nnabscl  9927  abssub  9928  abstri  9931  abs2dif  9933  abs2difabs  9935  abs3lem  9938  cau3lem  9941  cau4  9943  caubnd2  9944  rpsqrtcld  9985  leabsd  9988  absred  9989  abscld  10008  absvalsqd  10009  absvalsq2d  10010  absge0d  10011  absval2d  10012  absnegd  10016  abscjd  10017  releabsd  10018  clim  10033  clim2  10035  climi  10039  climi2  10040  climi0  10041  climconst  10042  climmpt  10052  2clim  10053  climshftlemg  10054  climshft2  10058  climabs0  10059  subcn2  10063  cn1lem  10065  recn2  10068  imcn2  10069  climcn1lem  10070  climrecl  10075  climge0  10076  climadd  10077  climmul  10078  climsub  10079  climaddc2  10081  clim2iser  10088  clim2iser2  10089  iiserex  10090  iserige0  10094  climub  10095  climserile  10096  climcau  10097  climcvg1nlem  10099  climcaucn  10101  serif0  10102  sumeq1  10105  moddvds  10117  dvds1lem  10119  dvds2lem  10120  summodnegmod  10138  modmulconst  10139  dvds2ln  10140  dvdslelemd  10155  dvdsabseq  10159  divconjdvds  10161  dvdsdivcl  10162  dvdsssfz1  10164  dvds1  10165  alzdvds  10166  dvdsext  10167  fzo0dvdseq  10169  fzocongeq  10170  addmodlteqALT  10171  dvdsfac  10172  dvdsmod  10174  mulmoddvds  10175  zeo3  10179  zeo4  10181  odd2np1lem  10183  odd2np1  10184  oexpneg  10188  oddnn02np1  10192  oddge22np1  10193  2tp1odd  10196  zob  10203  ltoddhalfle  10205  opoe  10207  opeo  10209  omeo  10210  nn0ehalf  10215  nno  10218  nn0ob  10220  nn0oddm1d2  10221  nnoddm1d2  10222  divalglemnqt  10232  divalgmod  10239  flodddiv4  10246  flodddiv4t2lthalf  10249  sqr2irrlem  10250  sqrt2irr  10251  pw2dvdslemn  10253  pw2dvdseulemle  10255  oddpwdclemxy  10257  oddpwdclemdvds  10258  oddpwdclemndvds  10259  oddpwdclemodd  10260  oddpwdclemdc  10261  oddpwdc  10262  ialgr0  10266  ialginv  10269  ialgcvg  10270  algcvgblem  10271  algcvgb  10272  ialgcvga  10273  elabgft1  10304  bj-rspgt  10312  bj-nalset  10402  bj-inex  10414  bj-sels  10421  bj-unexg  10428  bj-notbid  10434  bj-indind  10443  peano5setOLD  10452  speano5  10456  findset  10457  bj-bdfindisg  10460  bj-nn0suc  10476  bj-inf2vnlem1  10482  bj-inf2vn  10486  bj-inf2vn2  10487  bj-findis  10491  bj-findisg  10492
  Copyright terms: Public domain W3C validator