Intuitionistic Logic Explorer Home Intuitionistic Logic Explorer
Bibliographic Cross-References
 
Mirrors  >  Home  >  ILE Home  >  Bibliographic Cross-References

Bibliographic Cross-References   This table collects in one place the bibliographic references made in the Intuitionistic Logic Explorer's axiom, definition, and theorem Descriptions. If you are studying a particular reference, this list can be handy for finding out where any corresponding Metamath theorems might be located. Keep in mind that we usually give only one reference for a theorem that may appear in several books, so it can also be useful to browse the Related Theorems around a theorem of interest.

Bibliographic Cross-Reference for the Higher-Order Logic Explorer
Bibliographic Reference DescriptionHigher-Order Logic Explorer Page(s)
[Bauer] p. 482Example by pm2.65 566
[BellMachover] p. 36Lemma 10.3id1 18
[BellMachover] p. 97Definition 10.1df-eu 1815
[BellMachover] p. 460Notationdf-mo 1816
[BellMachover] p. 460Definitionmo3 1862
[Crosilla] (with unnnecessary quantifiers removed). Set theory can also be formulated with a _single_ primitive predicate ` ` on top of traditional predicate calculus _without_ equality. In that case the Axiom of Extensionality becomes ` ` , and equality ` ` is _defined_ as ` ` . All of the usual axioms of equality then become theorems of set theory. See, for example, Axiom 1 of [TakeutiZaring] p. 8Axiom 1ax-ext 1906
[Crosilla] p. Axiom 6ru 2620
[Hamilton] p. 31Example 2.7(a)id1 18
[Hamilton] p. 73Rule 1ax-mp 7
[Hamilton] p. 74Rule 2ax-gen 1274
[Hitchcock] p. 5Rule A3mpto1 1251
[Hitchcock] p. 5Rule A4mpto2 1252
[Hitchcock] p. 5Rule A5mtp-xor 1253
[Jech] p. 4Definition of classcvjust 1918
[KalishMontague] p. 81Axiom B7' in footnote 1ax-i9 1360
[Kunen] p. 10Axiom 0a9e 1506
[Levy] p. 338Axiomdf-clab 1910  df-clel 1919  df-cleq 1916
[Lopez-Astorga] p. 12Rule 1mpto1 1251
[Lopez-Astorga] p. 12Rule 2mpto2 1252
[Lopez-Astorga] p. 12Rule 3mtp-xor 1253
[Margaris] p. 40Rule Cexlimiv 1424
[Margaris] p. 49Axiom A1ax-1 5
[Margaris] p. 49Axiom A2ax-2 6
[Margaris] p. 49Axiom A3ax-3 2621
[Margaris] p. 49Definitiondf-ex 2645  df-or 2642  dfbi2 365  dfordc 764
[Margaris] p. 51Theorem 1id1 18
[Margaris] p. 56Theorem 3syld 38
[Margaris] p. 60Theorem 8mth8 560
[Margaris] p. 89Theorem 19.219.2 1461
[Margaris] p. 89Theorem 19.319.3 1384  19.3h 1383  rr19.3v 2541
[Margaris] p. 89Theorem 19.5alcom 1302
[Margaris] p. 89Theorem 19.6alex 2646  alexdc 1444  alexim 1466
[Margaris] p. 89Theorem 19.7alnex 1325
[Margaris] p. 89Theorem 19.819.8a 1417  spsbe 1641
[Margaris] p. 89Theorem 19.919.9 1465  19.9h 1464  19.9v 1668  exlimd 1423
[Margaris] p. 89Theorem 19.11excom 1480  excomim 1479
[Margaris] p. 89Theorem 19.1219.12 1481  r19.12 2287
[Margaris] p. 90Theorem 19.14exnal 2682
[Margaris] p. 90Theorem 19.15albi 1293  ralbi 2310
[Margaris] p. 90Theorem 19.1619.16 1385
[Margaris] p. 90Theorem 19.1719.17 1386
[Margaris] p. 90Theorem 19.18exbi 1430
[Margaris] p. 90Theorem 19.1919.19 1482
[Margaris] p. 90Theorem 19.20alim 1282  alimd 1351  alimdh 1292  alimdv 1675  ralimdaa 2251  ralimdv 2253  ralimdva 2252
[Margaris] p. 90Theorem 19.2119.21-2 1388  19.21 1412  19.21bi 1390  19.21h 1387  19.21ht 1410  19.21t 1411  19.21v 1669  alrimd 1436  alrimdd 1435  alrimdh 1303  alrimdv 1672  alrimi 1352  alrimih 1294  alrimiv 1670  alrimivv 1671  r19.21 2260  r19.21be 2275  r19.21bi 2272  r19.21t 2259  r19.21v 2261  ralrimd 2262  ralrimdv 2263  ralrimdva 2264  ralrimdvv 2268  ralrimdvva 2269  ralrimi 2255  ralrimiv 2256  ralrimiva 2257  ralrimivv 2265  ralrimivva 2266  ralrimivvva 2267  ralrimivw 2258  rexlimi 2291
[Margaris] p. 90Theorem 19.222alimdv 1677  2eximdv 1678  exim 1425  eximd 1438  eximdh 1437  eximdv 1676  rexim 2278  reximdai 2282  reximdv 2285  reximdv2 2283  reximdva 2286  reximdvai 2284  reximi2 2280
[Margaris] p. 90Theorem 19.2319.23 1324  19.23bi 1418  19.23ht 1323  19.23t 1490  19.23v 1679  19.23vv 1680  exlimd2 1421  exlimdh 1422  exlimdv 1618  exlimdvv 1693  exlimi 1420  exlimih 1419  exlimiv 1424  exlimivv 1692  r19.23 2289  r19.23v 2290  rexlimd 2295  rexlimdv 2297  rexlimdv3a 2300  rexlimdva 2298  rexlimdvaa 2299  rexlimdvv 2304  rexlimdvva 2305  rexlimdvw 2301  rexlimiv 2292  rexlimiva 2293  rexlimivv 2303
[Margaris] p. 90Theorem 19.2419.24 2680
[Margaris] p. 90Theorem 19.2519.25 1451
[Margaris] p. 90Theorem 19.2619.26-2 1307  19.26-3an 1308  19.26 1305  r19.26-2 2307  r19.26-3 2308  r19.26 2306  r19.26m 2309
[Margaris] p. 90Theorem 19.2719.27 1392  19.27v 1694  r19.27av 2312
[Margaris] p. 90Theorem 19.2819.28 1393  19.28v 1695  r19.28av 2313  rr19.28v 2542
[Margaris] p. 90Theorem 19.2919.29 1445  19.29r 1446  19.29r2 1447  19.29x 1448  r19.29 2314  r19.29d2r 2319  r19.29r 2315
[Margaris] p. 90Theorem 19.3019.30 2687
[Margaris] p. 90Theorem 19.3119.31 2652
[Margaris] p. 90Theorem 19.3219.32 2651  19.32dc 1491  r19.32vdc 2321
[Margaris] p. 90Theorem 19.3319.33 1309  19.33b2 1453  19.33bdc 1454
[Margaris] p. 90Theorem 19.3419.34 1494
[Margaris] p. 90Theorem 19.3519.35-1 1449  19.35 2653  19.35i 1450  19.35ri 2688
[Margaris] p. 90Theorem 19.3619.36-1 1486  19.36 2677  19.36aiv 1696  19.36i 1485  19.36v 2678  r19.36av 2323
[Margaris] p. 90Theorem 19.3719.37-1 1487  19.37 2654  19.37aiv 1488  19.37v 2655  r19.37 2324  r19.37av 2325
[Margaris] p. 90Theorem 19.3819.38 1489
[Margaris] p. 90Theorem 19.3919.39 2679
[Margaris] p. 90Theorem 19.4019.40-2 1456  19.40 1455  r19.40 2326
[Margaris] p. 90Theorem 19.4119.41 1496  19.41h 1495  19.41v 1697  19.41vv 1698  19.41vvv 1699  19.41vvvv 1700  r19.41 2327  r19.41v 2328
[Margaris] p. 90Theorem 19.4219.42 1498  19.42h 1497  19.42v 1701  19.42vv 1703  19.42vvv 1704  r19.42v 2329
[Margaris] p. 90Theorem 19.4319.43 1452  r19.43 2330
[Margaris] p. 90Theorem 19.4419.44 1492  r19.44av 2331
[Margaris] p. 90Theorem 19.4519.45 1493  r19.45av 2332
[Margaris] p. 110Exercise 2(b)eu1 1835
[Megill] p. 444Axiom C5ax-17 1356
[Megill] p. 445Lemma L12alequcom 1345  ax-10 1334
[Megill] p. 446Lemma L17equtrr 1514
[Megill] p. 446Lemma L19hbnae 1527
[Megill] p. 447Remark 9.1df-sb 1565  sbid 1576
[Megill] p. 448Scheme C5'ax-4 1338
[Megill] p. 448Scheme C6'ax-7 1273
[Megill] p. 448Scheme C8'ax-8 1333
[Megill] p. 448Scheme C9'ax-i12 1336
[Megill] p. 448Scheme C11'ax-10o 1522
[Megill] p. 448Scheme C12'ax-13 1342
[Megill] p. 448Scheme C13'ax-14 1343
[Megill] p. 448Scheme C15'ax-11o 1622
[Megill] p. 448Scheme C16'ax-16 1613
[Megill] p. 448Theorem 9.4dral1 1535  dral2 1536  drex1 1597  drex2 1537  drsb1 1598  drsb2 1640
[Megill] p. 449Theorem 9.7sbcom2 1776  sbequ 1639  sbid2v 1786
[Megill] p. 450Example in Appendixhba1 1371
[Mendelson] p. 36Lemma 1.8id1 18
[Mendelson] p. 69Axiom 4stdpc4 1577
[Mendelson] p. 69Axiom 5stdpc5 1389
[Mendelson] p. 81Rule Cexlimiv 1424
[Mendelson] p. 95Axiom 6stdpc6 1509
[Mendelson] p. 95Axiom 7stdpc7 1572
[Monk2] p. 105Axiom C4ax-5 1272
[Monk2] p. 105Axiom C7ax-8 1333
[Monk2] p. 105Axiom C8ax-11 1335  ax-11o 1622
[Monk2] p. 105Axiom (C8)ax11v 1626
[Monk2] p. 109Lemma 12ax-7 1273
[Monk2] p. 109Lemma 15equvin 1660  equvini 1559
[Monk2] p. 113Axiom C5-1ax-17 1356
[Monk2] p. 113Axiom C5-2ax6b 1468
[Monk2] p. 113Axiom C5-3ax-7 1273
[Monk2] p. 114Lemma 22hba1 1371
[Monk2] p. 114Lemma 23hbia1 1382  nfia1 1409
[Monk2] p. 114Lemma 24hba2 1381  nfa2 1408
[Quine] p. 16Definition 2.1df-clab 1910  rabid 2347
[Quine] p. 17Definition 2.1''dfsb7 1781
[Quine] p. 18Definition 2.7df-cleq 1916
[Quine] p. 19Definition 2.9df-v 2420
[Quine] p. 34Theorem 5.1abeq2 2028
[Quine] p. 35Theorem 5.2abid2 2040  abid2f 2083
[Quine] p. 40Theorem 6.1sb5 1683
[Quine] p. 40Theorem 6.2sb56 1681  sb6 1682
[Quine] p. 41Theorem 6.3df-clel 1919
[Quine] p. 41Theorem 6.4eqid 1923
[Quine] p. 41Theorem 6.5eqcom 1925
[Quine] p. 43Theorem 6.8vex 2421
[Quine] p. 43Theorem 6.9isset 2422
[Quine] p. 44Theorem 7.3spcgf 2495  spcgv 2500  spcimgf 2493
[Quine] p. 44Theorem 6.12elex 2426
[Quine] p. 44Theorem 6.13elab 2546  elabg 2547  elabgf 2544
[Sanford] p. 39Rule 3mtp-xor 1253
[Sanford] p. 39Rule 4mpto2 1252
[Sanford] p. 40Rule 1mpto1 1251
[Stoll] p. 176Theorem 3.4(27)iman 2639  imandc 759
[TakeutiZaring] p. 8Axiom 1ax-ext 1906
[TakeutiZaring] p. 13Definition 4.5df-cleq 1916
[TakeutiZaring] p. 13Proposition 4.6df-clel 1919
[TakeutiZaring] p. 13Proposition 4.9cvjust 1918
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 1940
[TakeutiZaring] p. 14Proposition 4.14ru 2620
[TakeutiZaring] p. 20Definitiondf-rab 2184
[TakeutiZaring] p. 21Definition 5.20df-v 2420
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2180
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2181
[TakeutiZaring] p. 26Definition 6.10eu2 1854
[TakeutiZaring] p. 53Proposition 7.532eu5 2667
[Tarski] p. 67Axiom B5ax-4 1338
[Tarski] p. 68Lemma 6equid 1508
[Tarski] p. 69Lemma 7equcomi 1510
[Tarski] p. 70Lemma 14spim 1543  spime 1546  spimeh 1544  spimh 1542
[Tarski] p. 70Lemma 16ax-11 1335  ax-11o 1622  ax11i 1520
[Tarski] p. 70Lemmas 16 and 17sb6 1682
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1356
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax-13 1342  ax-14 1343
[WhiteheadRussell] p. 96Axiom *1.3olc 612
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 625
[WhiteheadRussell] p. 96Axiom *1.2 (Taut)pm1.2 652
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 661
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 682
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 529  pm2.01 529
[WhiteheadRussell] p. 100Theorem *2.02ax-1 5
[WhiteheadRussell] p. 100Theorem *2.03con2 553
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 74
[WhiteheadRussell] p. 100Theorem *2.05imim2 47
[WhiteheadRussell] p. 100Theorem *2.06imim1 68
[WhiteheadRussell] p. 101Theorem *2.1pm2.1dc 721
[WhiteheadRussell] p. 101Theorem *2.06syl 13
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 635
[WhiteheadRussell] p. 101Theorem *2.08id 17  id1 18
[WhiteheadRussell] p. 101Theorem *2.11exmiddc 720
[WhiteheadRussell] p. 101Theorem *2.12notnot1 542
[WhiteheadRussell] p. 101Theorem *2.13pm2.13dc 753
[WhiteheadRussell] p. 102Theorem *2.14notnot2 2631
[WhiteheadRussell] p. 102Theorem *2.15con1dc 727
[WhiteheadRussell] p. 103Theorem *2.16con3 552
[WhiteheadRussell] p. 103Theorem *2.17ax-3 2621
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 2624  pm2.18dc 725
[WhiteheadRussell] p. 104Theorem *2.2orc 613
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 671
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 530
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 534
[WhiteheadRussell] p. 104Theorem *2.25pm2.25dc 765
[WhiteheadRussell] p. 104Theorem *2.26pm2.26dc 782
[WhiteheadRussell] p. 104Theorem *2.27pm2.27 33
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 664
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 665
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 695
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 696
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 694
[WhiteheadRussell] p. 105Definition *2.33df-3or 848
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 674
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 672
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 673
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 45
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 636
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 637
[WhiteheadRussell] p. 107Theorem *2.5pm2.5dc 737
[WhiteheadRussell] p. 107Theorem *2.6pm2.6dc 733
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 638
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 639
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 640
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 562
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 563
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 620
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 2641  pm2.54dc 763
[WhiteheadRussell] p. 107Theorem *2.55orel1 623
[WhiteheadRussell] p. 107Theorem *2.56orel2 624
[WhiteheadRussell] p. 107Theorem *2.61pm2.61dc 736
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 646
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 691
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 692
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 566
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 614  pm2.67 641
[WhiteheadRussell] p. 107Theorem *2.521pm2.521dc 738
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 645
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 701
[WhiteheadRussell] p. 108Theorem *2.68pm2.68dc 766
[WhiteheadRussell] p. 108Theorem *2.69looinvdc 790
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 697
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 698
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 700
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 699
[WhiteheadRussell] p. 108Theorem *2.77ax-2 6
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 702
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 703
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 69
[WhiteheadRussell] p. 108Theorem *2.85pm2.85dc 780
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 92
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 650
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 124
[WhiteheadRussell] p. 111Theorem *3.11pm3.11dc 830
[WhiteheadRussell] p. 111Theorem *3.12pm3.12dc 831
[WhiteheadRussell] p. 111Theorem *3.13pm3.13dc 832
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 649
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 249
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 250
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 608
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 326
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 246
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 247
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 100  simplim 2650  simplimdc 731
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 101  simprimdc 730
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 324
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 325
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37dc 761
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 314
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 312
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 313
[WhiteheadRussell] p. 113Theorem *3.44jao 651  pm3.44 615
[WhiteheadRussell] p. 113Theorem *3.47prth 323
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 516
[WhiteheadRussell] p. 113Theorem *3.45 (Fact)pm3.45 511
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 678
[WhiteheadRussell] p. 116Theorem *4.1con34bdc 739
[WhiteheadRussell] p. 117Theorem *4.2biid 158
[WhiteheadRussell] p. 117Theorem *4.11notbi 2635
[WhiteheadRussell] p. 117Theorem *4.13notnot 2632  notnotdc 740
[WhiteheadRussell] p. 117Theorem *4.14pm4.14dc 760
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 762
[WhiteheadRussell] p. 117Theorem *4.21bicom 126
[WhiteheadRussell] p. 117Theorem *4.22biantr 825  bitr 439
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 371
[WhiteheadRussell] p. 117Theorem *4.25oridm 653  pm4.25 654
[WhiteheadRussell] p. 118Theorem *4.3ancom 251
[WhiteheadRussell] p. 118Theorem *4.4andi 710
[WhiteheadRussell] p. 118Theorem *4.31orcom 626
[WhiteheadRussell] p. 118Theorem *4.32anass 379
[WhiteheadRussell] p. 118Theorem *4.33orass 663
[WhiteheadRussell] p. 118Theorem *4.36anbi1 437
[WhiteheadRussell] p. 118Theorem *4.37orbi1 685
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 520
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 714
[WhiteheadRussell] p. 118Definition *4.34df-3an 849
[WhiteheadRussell] p. 119Theorem *4.41ordi 708
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 822
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 675
[WhiteheadRussell] p. 119Theorem *4.45orabs 705  pm4.45 677  pm4.45im 315
[WhiteheadRussell] p. 119Theorem *10.2219.26 1305
[WhiteheadRussell] p. 120Theorem *4.5anordc 829
[WhiteheadRussell] p. 120Theorem *4.6imor 2643  imordc 769
[WhiteheadRussell] p. 120Theorem *4.7anclb 300
[WhiteheadRussell] p. 120Theorem *4.51ianordc 771
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 2670
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 2671
[WhiteheadRussell] p. 120Theorem *4.54pm4.54dc 775
[WhiteheadRussell] p. 120Theorem *4.55pm4.55dc 807
[WhiteheadRussell] p. 120Theorem *4.56ioran 648  pm4.56 776
[WhiteheadRussell] p. 120Theorem *4.57oran 2672  pm4.57 2673
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 2674
[WhiteheadRussell] p. 120Theorem *4.62pm4.62dc 770
[WhiteheadRussell] p. 120Theorem *4.63pm4.63dc 754
[WhiteheadRussell] p. 120Theorem *4.64pm4.64dc 773
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 2675
[WhiteheadRussell] p. 120Theorem *4.66pm4.66dc 774
[WhiteheadRussell] p. 120Theorem *4.67pm4.67dc 755
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 366  pm4.71i 368  pm4.71r 367  pm4.71rd 370  pm4.71ri 369
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 715
[WhiteheadRussell] p. 121Theorem *4.73iba 282
[WhiteheadRussell] p. 121Theorem *4.74biorf 642
[WhiteheadRussell] p. 121Theorem *4.76jcab 517  pm4.76 519
[WhiteheadRussell] p. 121Theorem *4.77jaob 611  pm4.77 690
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 2676
[WhiteheadRussell] p. 121Theorem *4.79pm4.79dc 778
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 604
[WhiteheadRussell] p. 122Theorem *4.81pm4.81dc 783
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 823
[WhiteheadRussell] p. 122Theorem *4.83pm4.83dc 824
[WhiteheadRussell] p. 122Theorem *4.84imbi1 223
[WhiteheadRussell] p. 122Theorem *4.85imbi2 224
[WhiteheadRussell] p. 122Theorem *4.86bibi1 227
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 235  impexp 248  pm4.87 476
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 515
[WhiteheadRussell] p. 123Theorem *5.11pm5.11dc 784
[WhiteheadRussell] p. 123Theorem *5.12pm5.12dc 785
[WhiteheadRussell] p. 123Theorem *5.13pm5.13dc 787
[WhiteheadRussell] p. 123Theorem *5.14pm5.14dc 786
[WhiteheadRussell] p. 124Theorem *5.15pm5.15dc 1219
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 716
[WhiteheadRussell] p. 124Theorem *5.17pm5.17dc 779
[WhiteheadRussell] p. 124Theorem *5.18nbbndc 1224  pm5.18dc 751
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 603
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 592
[WhiteheadRussell] p. 124Theorem *5.22xordc 1222
[WhiteheadRussell] p. 124Theorem *5.23dfbi3dc 1227
[WhiteheadRussell] p. 124Theorem *5.24pm5.24dc 1228
[WhiteheadRussell] p. 124Theorem *5.25dfor2dc 767
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 442
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 236
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 229
[WhiteheadRussell] p. 125Theorem *5.6pm5.6dc 797
[WhiteheadRussell] p. 125Theorem *5.7pm5.7dc 827
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 327
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 425
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 524
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 792
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 525
[WhiteheadRussell] p. 125Theorem *5.41imdi 237  pm5.41 238
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 301
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 796
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 693
[WhiteheadRussell] p. 125Theorem *5.54pm5.54dc 793
[WhiteheadRussell] p. 125Theorem *5.55pm5.55dc 788
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 687
[WhiteheadRussell] p. 125Theorem *5.62pm5.62dc 818
[WhiteheadRussell] p. 125Theorem *5.63pm5.63dc 819
[WhiteheadRussell] p. 125Theorem *5.71pm5.71dc 834
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 231
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 166
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 835
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 1777
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1310
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1456
[WhiteheadRussell] p. 164Theorem *11.52nalexn 2683
[WhiteheadRussell] p. 164Theorem *11.512exnexn 2685
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1691
[WhiteheadRussell] p. 175Definition *14.02df-eu 1815
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2157
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2158
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2540
[WhiteheadRussell] p. 192Theorem *14.26eupick 1888  eupickbi 1891

  This page was last updated on 14-Aug-2016.
Copyright terms: Public domain
W3C HTML validation [external]