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 1780
[BellMachover] p. 460Notationdf-mo 1781
[BellMachover] p. 460Definitionmo3 2112
[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 1793
[Hamilton] p. 31Example 2.7(a)id1 18
[Hamilton] p. 73Rule 1ax-mp 7
[Hamilton] p. 74Rule 2ax-gen 1269
[Hitchcock] p. 5Rule A3mpto1 1246
[Hitchcock] p. 5Rule A4mpto2 1247
[Hitchcock] p. 5Rule A5mtp-xor 1248
[Jech] p. 4Definition of classcvjust 1805
[KalishMontague] p. 81Axiom B7' in footnote 1ax-i9 1354
[Kunen] p. 10Axiom 0a9e 1478
[Levy] p. 338Axiomdf-clab 1797  df-clel 1806  df-cleq 1803
[Lopez-Astorga] p. 12Rule 1mpto1 1246
[Lopez-Astorga] p. 12Rule 2mpto2 1247
[Lopez-Astorga] p. 12Rule 3mtp-xor 1248
[Margaris] p. 40Rule Cexlimiv 1412
[Margaris] p. 49Axiom A1ax-1 5
[Margaris] p. 49Axiom A2ax-2 6
[Margaris] p. 49Axiom A3ax-3 2062
[Margaris] p. 49Definitiondf-ex 2086  df-or 2083  dfbi2 365  dfordc 763
[Margaris] p. 51Theorem 1id1 18
[Margaris] p. 56Theorem 3syld 38
[Margaris] p. 60Theorem 8mth8 560
[Margaris] p. 89Theorem 19.219.2 1442
[Margaris] p. 89Theorem 19.319.3 1377
[Margaris] p. 89Theorem 19.5alcom 1297
[Margaris] p. 89Theorem 19.6alex 2087
[Margaris] p. 89Theorem 19.7alnex 1320
[Margaris] p. 89Theorem 19.819.8a 1407  a4sbe 1609
[Margaris] p. 89Theorem 19.919.9 1445  19.9v 1636
[Margaris] p. 89Theorem 19.11excom 1459  excomim 1458
[Margaris] p. 89Theorem 19.1219.12 1460
[Margaris] p. 90Theorem 19.14exnal 2187
[Margaris] p. 90Theorem 19.15albi 1288
[Margaris] p. 90Theorem 19.1619.16 1378
[Margaris] p. 90Theorem 19.1719.17 1379
[Margaris] p. 90Theorem 19.18exbi 1417
[Margaris] p. 90Theorem 19.1919.19 1461
[Margaris] p. 90Theorem 19.20alim 1277  alimd 1287  alimdv 1643
[Margaris] p. 90Theorem 19.2119.21-2 1381  19.21 1380  19.21bi 1383  19.21ht 1401  19.21t 1402  19.21v 1637  alrimd 1298  alrimdv 1640  alrimi 1346  alrimih 1289  alrimiv 1638  alrimivv 1639
[Margaris] p. 90Theorem 19.222alimdv 1645  2eximdv 1646  exim 1413  eximd 1422  eximdv 1644
[Margaris] p. 90Theorem 19.2319.23 1319  19.23bi 1408  19.23t 1318  19.23v 1647  19.23vv 1648  exlimd 1411  exlimd2 1410  exlimdv 1586  exlimdvv 1661  exlimi 1409  exlimiv 1412  exlimivv 1660
[Margaris] p. 90Theorem 19.2419.24 2185
[Margaris] p. 90Theorem 19.2519.25 1432
[Margaris] p. 90Theorem 19.2619.26-2 1302  19.26-3an 1303  19.26 1300
[Margaris] p. 90Theorem 19.2719.27 1385  19.27v 1662
[Margaris] p. 90Theorem 19.2819.28 1386  19.28v 1663
[Margaris] p. 90Theorem 19.2919.29 1426  19.29r 1427  19.29r2 1428  19.29x 1429
[Margaris] p. 90Theorem 19.3019.30 2192
[Margaris] p. 90Theorem 19.3119.31 2094
[Margaris] p. 90Theorem 19.3219.32 2093
[Margaris] p. 90Theorem 19.3319.33 1304  19.33b2 1434  19.33bdc 1435
[Margaris] p. 90Theorem 19.3419.34 1468
[Margaris] p. 90Theorem 19.3519.35-1 1430  19.35 2095  19.35i 1431  19.35ri 2193
[Margaris] p. 90Theorem 19.3619.36 2182  19.36aiv 1664  19.36i 1464  19.36v 2183
[Margaris] p. 90Theorem 19.3719.37 2096  19.37v 2097
[Margaris] p. 90Theorem 19.3819.38 1465
[Margaris] p. 90Theorem 19.3919.39 2184
[Margaris] p. 90Theorem 19.4019.40-2 1437  19.40 1436
[Margaris] p. 90Theorem 19.4119.41 1469  19.41v 1665  19.41vv 1666  19.41vvv 1667  19.41vvvv 1668
[Margaris] p. 90Theorem 19.4219.42 1470  19.42v 1669  19.42vv 1671  19.42vvv 1672
[Margaris] p. 90Theorem 19.4319.43 1433
[Margaris] p. 90Theorem 19.4419.44 1466
[Margaris] p. 90Theorem 19.4519.45 1467
[Margaris] p. 110Exercise 2(b)eu1 2102
[Megill] p. 444Axiom C5ax-17 1350
[Megill] p. 445Lemma L12alequcom 1340  ax-10 1329
[Megill] p. 446Lemma L17equtrr 1486
[Megill] p. 446Lemma L19hbnae 1499
[Megill] p. 447Remark 9.1df-sb 1533  sbid 1544
[Megill] p. 448Scheme C5'ax-4 1333
[Megill] p. 448Scheme C6'ax-7 1268
[Megill] p. 448Scheme C8'ax-8 1328
[Megill] p. 448Scheme C9'ax-i12 1331
[Megill] p. 448Scheme C11'ax-10o 1494
[Megill] p. 448Scheme C12'ax-13 1337
[Megill] p. 448Scheme C13'ax-14 1338
[Megill] p. 448Scheme C15'ax-11o 1590
[Megill] p. 448Scheme C16'ax-16 1581
[Megill] p. 448Theorem 9.4dral1 1507  dral2 1508  drex1 1565  drex2 1509  drsb1 1566  drsb2 1608
[Megill] p. 449Theorem 9.7sbcom2 1741  sbequ 1607  sbid2v 1751
[Megill] p. 450Example in Appendixhba1 1365
[Mendelson] p. 36Lemma 1.8id1 18
[Mendelson] p. 69Axiom 4stdpc4 1545
[Mendelson] p. 69Axiom 5stdpc5 1382
[Mendelson] p. 81Rule Cexlimiv 1412
[Mendelson] p. 95Axiom 6stdpc6 1481
[Mendelson] p. 95Axiom 7stdpc7 1540
[Monk2] p. 105Axiom C4ax-5 1267
[Monk2] p. 105Axiom C7ax-8 1328
[Monk2] p. 105Axiom C8ax-11 1330  ax-11o 1590
[Monk2] p. 105Axiom (C8)ax11v 1594
[Monk2] p. 109Lemma 12ax-7 1268
[Monk2] p. 109Lemma 15equvin 1628  equvini 1525
[Monk2] p. 113Axiom C5-1ax-17 1350
[Monk2] p. 113Axiom C5-2ax6b 1447
[Monk2] p. 113Axiom C5-3ax-7 1268
[Monk2] p. 114Lemma 22hba1 1365
[Monk2] p. 114Lemma 23hbia1 1376  nfia1 1530
[Monk2] p. 114Lemma 24hba2 1375  nfa2 1529
[Quine] p. 16Definition 2.1df-clab 1797
[Quine] p. 17Definition 2.1''dfsb7 1746
[Quine] p. 18Definition 2.7df-cleq 1803
[Quine] p. 34Theorem 5.1abeq2 1915
[Quine] p. 35Theorem 5.2abid2 1927  abid2f 1970
[Quine] p. 40Theorem 6.1sb5 1651
[Quine] p. 40Theorem 6.2sb56 1649  sb6 1650
[Quine] p. 41Theorem 6.3df-clel 1806
[Quine] p. 41Theorem 6.4eqid 1810
[Quine] p. 41Theorem 6.5eqcom 1812
[Sanford] p. 39Rule 3mtp-xor 1248
[Sanford] p. 39Rule 4mpto2 1247
[Sanford] p. 40Rule 1mpto1 1246
[Stoll] p. 176Theorem 3.4(27)iman 2080  imandc 758
[TakeutiZaring] p. 8Axiom 1ax-ext 1793
[TakeutiZaring] p. 13Definition 4.5df-cleq 1803
[TakeutiZaring] p. 13Proposition 4.6df-clel 1806
[TakeutiZaring] p. 13Proposition 4.9cvjust 1805
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 1827
[TakeutiZaring] p. 26Definition 6.10eu2 2106
[TakeutiZaring] p. 53Proposition 7.532eu5 2166
[Tarski] p. 67Axiom B5ax-4 1333
[Tarski] p. 68Lemma 6equid 1480
[Tarski] p. 69Lemma 7equcomi 1482
[Tarski] p. 70Lemma 14a4im 1513  a4ime 1514
[Tarski] p. 70Lemma 16ax-11 1330  ax-11o 1590  ax11i 1492
[Tarski] p. 70Lemmas 16 and 17sb6 1650
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1350
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax-13 1337  ax-14 1338
[WhiteheadRussell] p. 96Axiom *1.3olc 611
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 624
[WhiteheadRussell] p. 96Axiom *1.2 (Taut)pm1.2 651
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 660
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 681
[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 720
[WhiteheadRussell] p. 101Theorem *2.06syl 13
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 634
[WhiteheadRussell] p. 101Theorem *2.08id 17  id1 18
[WhiteheadRussell] p. 101Theorem *2.11exmiddc 719
[WhiteheadRussell] p. 101Theorem *2.12notnot1 542
[WhiteheadRussell] p. 101Theorem *2.13pm2.13dc 752
[WhiteheadRussell] p. 102Theorem *2.14notnot2 2072
[WhiteheadRussell] p. 102Theorem *2.15con1dc 726
[WhiteheadRussell] p. 103Theorem *2.16con3 552
[WhiteheadRussell] p. 103Theorem *2.17ax-3 2062
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 2065  pm2.18dc 724
[WhiteheadRussell] p. 104Theorem *2.2orc 612
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 670
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 530
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 534
[WhiteheadRussell] p. 104Theorem *2.25pm2.25dc 764
[WhiteheadRussell] p. 104Theorem *2.26pm2.26dc 781
[WhiteheadRussell] p. 104Theorem *2.27pm2.27 33
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 663
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 664
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 694
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 695
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 693
[WhiteheadRussell] p. 105Definition *2.33df-3or 844
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 673
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 671
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 672
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 45
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 635
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 636
[WhiteheadRussell] p. 107Theorem *2.5pm2.5dc 736
[WhiteheadRussell] p. 107Theorem *2.6pm2.6dc 732
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 637
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 638
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 639
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 562
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 563
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 619
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 2082  pm2.54dc 762
[WhiteheadRussell] p. 107Theorem *2.55orel1 622
[WhiteheadRussell] p. 107Theorem *2.56orel2 623
[WhiteheadRussell] p. 107Theorem *2.61pm2.61dc 735
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 645
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 690
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 691
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 566
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 613  pm2.67 640
[WhiteheadRussell] p. 107Theorem *2.521pm2.521dc 737
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 644
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 700
[WhiteheadRussell] p. 108Theorem *2.68pm2.68dc 765
[WhiteheadRussell] p. 108Theorem *2.69looinv 2181
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 696
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 697
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 699
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 698
[WhiteheadRussell] p. 108Theorem *2.77ax-2 6
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 701
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 702
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 69
[WhiteheadRussell] p. 108Theorem *2.85pm2.85dc 779
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 92
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 649
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 124
[WhiteheadRussell] p. 111Theorem *3.11pm3.11dc 826
[WhiteheadRussell] p. 111Theorem *3.12pm3.12dc 827
[WhiteheadRussell] p. 111Theorem *3.13pm3.13dc 828
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 648
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 249
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 250
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 607
[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 2091  simplimdc 730
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 101  simprimdc 729
[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 760
[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 650  pm3.44 614
[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 677
[WhiteheadRussell] p. 116Theorem *4.1con34bdc 738
[WhiteheadRussell] p. 117Theorem *4.2biid 158
[WhiteheadRussell] p. 117Theorem *4.11notbi 2076
[WhiteheadRussell] p. 117Theorem *4.13notnot 2073  notnotdc 739
[WhiteheadRussell] p. 117Theorem *4.14pm4.14dc 759
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 761
[WhiteheadRussell] p. 117Theorem *4.21bicom 126
[WhiteheadRussell] p. 117Theorem *4.22biantr 821  bitr 439
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 371
[WhiteheadRussell] p. 117Theorem *4.25oridm 652  pm4.25 653
[WhiteheadRussell] p. 118Theorem *4.3ancom 251
[WhiteheadRussell] p. 118Theorem *4.4andi 709
[WhiteheadRussell] p. 118Theorem *4.31orcom 625
[WhiteheadRussell] p. 118Theorem *4.32anass 379
[WhiteheadRussell] p. 118Theorem *4.33orass 662
[WhiteheadRussell] p. 118Theorem *4.36anbi1 437
[WhiteheadRussell] p. 118Theorem *4.37orbi1 684
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 520
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 713
[WhiteheadRussell] p. 118Definition *4.34df-3an 845
[WhiteheadRussell] p. 119Theorem *4.41ordi 707
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 818
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 674
[WhiteheadRussell] p. 119Theorem *4.45orabs 704  pm4.45 676  pm4.45im 315
[WhiteheadRussell] p. 119Theorem *10.2219.26 1300
[WhiteheadRussell] p. 120Theorem *4.5anordc 825
[WhiteheadRussell] p. 120Theorem *4.6imor 2084  imordc 768
[WhiteheadRussell] p. 120Theorem *4.7anclb 300
[WhiteheadRussell] p. 120Theorem *4.51ianordc 770
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 2174
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 2175
[WhiteheadRussell] p. 120Theorem *4.54pm4.54dc 774
[WhiteheadRussell] p. 120Theorem *4.55pm4.55dc 803
[WhiteheadRussell] p. 120Theorem *4.56ioran 647  pm4.56 775
[WhiteheadRussell] p. 120Theorem *4.57oran 2176  pm4.57 2177
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 2178
[WhiteheadRussell] p. 120Theorem *4.62pm4.62dc 769
[WhiteheadRussell] p. 120Theorem *4.63pm4.63dc 753
[WhiteheadRussell] p. 120Theorem *4.64pm4.64dc 772
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 2179
[WhiteheadRussell] p. 120Theorem *4.66pm4.66dc 773
[WhiteheadRussell] p. 120Theorem *4.67pm4.67dc 754
[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 714
[WhiteheadRussell] p. 121Theorem *4.73iba 282
[WhiteheadRussell] p. 121Theorem *4.74biorf 641
[WhiteheadRussell] p. 121Theorem *4.76jcab 517  pm4.76 519
[WhiteheadRussell] p. 121Theorem *4.77jaob 610  pm4.77 689
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 2180
[WhiteheadRussell] p. 121Theorem *4.79pm4.79dc 777
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 604
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 2173
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 819
[WhiteheadRussell] p. 122Theorem *4.83pm4.83dc 820
[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 782
[WhiteheadRussell] p. 123Theorem *5.12pm5.12dc 783
[WhiteheadRussell] p. 123Theorem *5.13pm5.13dc 785
[WhiteheadRussell] p. 123Theorem *5.14pm5.14dc 784
[WhiteheadRussell] p. 124Theorem *5.15pm5.15dc 1214
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 715
[WhiteheadRussell] p. 124Theorem *5.17pm5.17dc 778
[WhiteheadRussell] p. 124Theorem *5.18nbbndc 1219  pm5.18dc 750
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 603
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 592
[WhiteheadRussell] p. 124Theorem *5.22xordc 1217
[WhiteheadRussell] p. 124Theorem *5.23dfbi3dc 1222
[WhiteheadRussell] p. 124Theorem *5.24pm5.24dc 1223
[WhiteheadRussell] p. 124Theorem *5.25dfor2dc 766
[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 793
[WhiteheadRussell] p. 125Theorem *5.7pm5.7dc 823
[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 788
[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 792
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 692
[WhiteheadRussell] p. 125Theorem *5.54pm5.54dc 789
[WhiteheadRussell] p. 125Theorem *5.55pm5.55dc 786
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 686
[WhiteheadRussell] p. 125Theorem *5.62pm5.62dc 814
[WhiteheadRussell] p. 125Theorem *5.63pm5.63dc 815
[WhiteheadRussell] p. 125Theorem *5.71pm5.71dc 830
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 231
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 166
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 831
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 1742
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1305
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1437
[WhiteheadRussell] p. 164Theorem *11.52nalexn 2188
[WhiteheadRussell] p. 164Theorem *11.512exnexn 2190
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1659
[WhiteheadRussell] p. 175Definition *14.02df-eu 1780
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2044
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2045
[WhiteheadRussell] p. 192Theorem *14.26eupick 2145  eupickbi 2148

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