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 1807
[BellMachover] p. 460Notationdf-mo 1808
[BellMachover] p. 460Definitionmo3 2553
[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 1850
[Hamilton] p. 31Example 2.7(a)id1 18
[Hamilton] p. 73Rule 1ax-mp 7
[Hamilton] p. 74Rule 2ax-gen 1270
[Hitchcock] p. 5Rule A3mpto1 1247
[Hitchcock] p. 5Rule A4mpto2 1248
[Hitchcock] p. 5Rule A5mtp-xor 1249
[Jech] p. 4Definition of classcvjust 1862
[KalishMontague] p. 81Axiom B7' in footnote 1ax-i9 1356
[Kunen] p. 10Axiom 0a9e 1501
[Levy] p. 338Axiomdf-clab 1854  df-clel 1863  df-cleq 1860
[Lopez-Astorga] p. 12Rule 1mpto1 1247
[Lopez-Astorga] p. 12Rule 2mpto2 1248
[Lopez-Astorga] p. 12Rule 3mtp-xor 1249
[Margaris] p. 40Rule Cexlimiv 1420
[Margaris] p. 49Axiom A1ax-1 5
[Margaris] p. 49Axiom A2ax-2 6
[Margaris] p. 49Axiom A3ax-3 2512
[Margaris] p. 49Definitiondf-ex 2536  df-or 2533  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 1457
[Margaris] p. 89Theorem 19.319.3 1380  19.3h 1379  rr19.3v 2484
[Margaris] p. 89Theorem 19.5alcom 1298
[Margaris] p. 89Theorem 19.6alex 2537  alexdc 1440
[Margaris] p. 89Theorem 19.7alnex 1321
[Margaris] p. 89Theorem 19.819.8a 1413  a4sbe 1633
[Margaris] p. 89Theorem 19.919.9 1461  19.9h 1460  19.9v 1660  exlimd 1419
[Margaris] p. 89Theorem 19.11excom 1475  excomim 1474
[Margaris] p. 89Theorem 19.1219.12 1476  r19.12 2231
[Margaris] p. 90Theorem 19.14exnal 2612
[Margaris] p. 90Theorem 19.15albi 1289  ralbi 2254
[Margaris] p. 90Theorem 19.1619.16 1381
[Margaris] p. 90Theorem 19.1719.17 1382
[Margaris] p. 90Theorem 19.18exbi 1426
[Margaris] p. 90Theorem 19.1919.19 1477
[Margaris] p. 90Theorem 19.20alim 1278  alimd 1347  alimdh 1288  alimdv 1667  ralimdaa 2195  ralimdv 2197  ralimdva 2196
[Margaris] p. 90Theorem 19.2119.21-2 1384  19.21 1408  19.21bi 1386  19.21h 1383  19.21ht 1406  19.21t 1407  19.21v 1661  alrimd 1432  alrimdd 1431  alrimdh 1299  alrimdv 1664  alrimi 1348  alrimih 1290  alrimiv 1662  alrimivv 1663  r19.21 2204  r19.21be 2219  r19.21bi 2216  r19.21t 2203  r19.21v 2205  ralrimd 2206  ralrimdv 2207  ralrimdva 2208  ralrimdvv 2212  ralrimdvva 2213  ralrimi 2199  ralrimiv 2200  ralrimiva 2201  ralrimivv 2209  ralrimivva 2210  ralrimivvva 2211  ralrimivw 2202  rexlimi 2235
[Margaris] p. 90Theorem 19.222alimdv 1669  2eximdv 1670  exim 1421  eximd 1434  eximdh 1433  eximdv 1668  rexim 2222  reximdai 2226  reximdv 2229  reximdv2 2227  reximdva 2230  reximdvai 2228  reximi2 2224
[Margaris] p. 90Theorem 19.2319.23 1320  19.23bi 1414  19.23ht 1319  19.23t 1485  19.23v 1671  19.23vv 1672  exlimd2 1417  exlimdh 1418  exlimdv 1610  exlimdvv 1685  exlimi 1416  exlimih 1415  exlimiv 1420  exlimivv 1684  r19.23 2233  r19.23v 2234  rexlimd 2239  rexlimdv 2241  rexlimdv3a 2244  rexlimdva 2242  rexlimdvaa 2243  rexlimdvv 2248  rexlimdvva 2249  rexlimdvw 2245  rexlimiv 2236  rexlimiva 2237  rexlimivv 2247
[Margaris] p. 90Theorem 19.2419.24 2610
[Margaris] p. 90Theorem 19.2519.25 1447
[Margaris] p. 90Theorem 19.2619.26-2 1303  19.26-3an 1304  19.26 1301  r19.26-2 2251  r19.26-3 2252  r19.26 2250  r19.26m 2253
[Margaris] p. 90Theorem 19.2719.27 1388  19.27v 1686  r19.27av 2256
[Margaris] p. 90Theorem 19.2819.28 1389  19.28v 1687  r19.28av 2257  rr19.28v 2485
[Margaris] p. 90Theorem 19.2919.29 1441  19.29r 1442  19.29r2 1443  19.29x 1444  r19.29 2258  r19.29d2r 2263  r19.29r 2259
[Margaris] p. 90Theorem 19.3019.30 2617
[Margaris] p. 90Theorem 19.3119.31 2544
[Margaris] p. 90Theorem 19.3219.32 2543  19.32dc 1486  r19.32vdc 2265
[Margaris] p. 90Theorem 19.3319.33 1305  19.33b2 1449  19.33bdc 1450
[Margaris] p. 90Theorem 19.3419.34 1489
[Margaris] p. 90Theorem 19.3519.35-1 1445  19.35 2545  19.35i 1446  19.35ri 2618
[Margaris] p. 90Theorem 19.3619.36-1 1481  19.36 2607  19.36aiv 1688  19.36i 1480  19.36v 2608  r19.36av 2267
[Margaris] p. 90Theorem 19.3719.37-1 1482  19.37 2546  19.37aiv 1483  19.37v 2547  r19.37 2268  r19.37av 2269
[Margaris] p. 90Theorem 19.3819.38 1484
[Margaris] p. 90Theorem 19.3919.39 2609
[Margaris] p. 90Theorem 19.4019.40-2 1452  19.40 1451  r19.40 2270
[Margaris] p. 90Theorem 19.4119.41 1491  19.41h 1490  19.41v 1689  19.41vv 1690  19.41vvv 1691  19.41vvvv 1692  r19.41 2271  r19.41v 2272
[Margaris] p. 90Theorem 19.4219.42 1493  19.42h 1492  19.42v 1693  19.42vv 1695  19.42vvv 1696  r19.42v 2273
[Margaris] p. 90Theorem 19.4319.43 1448  r19.43 2274
[Margaris] p. 90Theorem 19.4419.44 1487  r19.44av 2275
[Margaris] p. 90Theorem 19.4519.45 1488  r19.45av 2276
[Margaris] p. 110Exercise 2(b)eu1 1827
[Megill] p. 444Axiom C5ax-17 1352
[Megill] p. 445Lemma L12alequcom 1341  ax-10 1330
[Megill] p. 446Lemma L17equtrr 1509
[Megill] p. 446Lemma L19hbnae 1522
[Megill] p. 447Remark 9.1df-sb 1557  sbid 1568
[Megill] p. 448Scheme C5'ax-4 1334
[Megill] p. 448Scheme C6'ax-7 1269
[Megill] p. 448Scheme C8'ax-8 1329
[Megill] p. 448Scheme C9'ax-i12 1332
[Megill] p. 448Scheme C11'ax-10o 1517
[Megill] p. 448Scheme C12'ax-13 1338
[Megill] p. 448Scheme C13'ax-14 1339
[Megill] p. 448Scheme C15'ax-11o 1614
[Megill] p. 448Scheme C16'ax-16 1605
[Megill] p. 448Theorem 9.4dral1 1530  dral2 1531  drex1 1589  drex2 1532  drsb1 1590  drsb2 1632
[Megill] p. 449Theorem 9.7sbcom2 1768  sbequ 1631  sbid2v 1778
[Megill] p. 450Example in Appendixhba1 1367
[Mendelson] p. 36Lemma 1.8id1 18
[Mendelson] p. 69Axiom 4stdpc4 1569
[Mendelson] p. 69Axiom 5stdpc5 1385
[Mendelson] p. 81Rule Cexlimiv 1420
[Mendelson] p. 95Axiom 6stdpc6 1504
[Mendelson] p. 95Axiom 7stdpc7 1564
[Monk2] p. 105Axiom C4ax-5 1268
[Monk2] p. 105Axiom C7ax-8 1329
[Monk2] p. 105Axiom C8ax-11 1331  ax-11o 1614
[Monk2] p. 105Axiom (C8)ax11v 1618
[Monk2] p. 109Lemma 12ax-7 1269
[Monk2] p. 109Lemma 15equvin 1652  equvini 1551
[Monk2] p. 113Axiom C5-1ax-17 1352
[Monk2] p. 113Axiom C5-2ax6b 1463
[Monk2] p. 113Axiom C5-3ax-7 1269
[Monk2] p. 114Lemma 22hba1 1367
[Monk2] p. 114Lemma 23hbia1 1378  nfia1 1405
[Monk2] p. 114Lemma 24hba2 1377  nfa2 1404
[Quine] p. 16Definition 2.1df-clab 1854  rabid 2291
[Quine] p. 17Definition 2.1''dfsb7 1773
[Quine] p. 18Definition 2.7df-cleq 1860
[Quine] p. 19Definition 2.9df-v 2363
[Quine] p. 34Theorem 5.1abeq2 1972
[Quine] p. 35Theorem 5.2abid2 1984  abid2f 2027
[Quine] p. 40Theorem 6.1sb5 1675
[Quine] p. 40Theorem 6.2sb56 1673  sb6 1674
[Quine] p. 41Theorem 6.3df-clel 1863
[Quine] p. 41Theorem 6.4eqid 1867
[Quine] p. 41Theorem 6.5eqcom 1869
[Quine] p. 43Theorem 6.8vex 2364
[Quine] p. 43Theorem 6.9isset 2365
[Quine] p. 44Theorem 7.3spcgf 2438  spcgv 2443  spcimgf 2436
[Quine] p. 44Theorem 6.12elex 2369
[Quine] p. 44Theorem 6.13elab 2489  elabg 2490  elabgf 2487
[Sanford] p. 39Rule 3mtp-xor 1249
[Sanford] p. 39Rule 4mpto2 1248
[Sanford] p. 40Rule 1mpto1 1247
[Stoll] p. 176Theorem 3.4(27)iman 2530  imandc 758
[TakeutiZaring] p. 8Axiom 1ax-ext 1850
[TakeutiZaring] p. 13Definition 4.5df-cleq 1860
[TakeutiZaring] p. 13Proposition 4.6df-clel 1863
[TakeutiZaring] p. 13Proposition 4.9cvjust 1862
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 1884
[TakeutiZaring] p. 20Definitiondf-rab 2128
[TakeutiZaring] p. 21Definition 5.20df-v 2363
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2124
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2125
[TakeutiZaring] p. 26Definition 6.10eu2 2549
[TakeutiZaring] p. 53Proposition 7.532eu5 2593
[Tarski] p. 67Axiom B5ax-4 1334
[Tarski] p. 68Lemma 6equid 1503
[Tarski] p. 69Lemma 7equcomi 1505
[Tarski] p. 70Lemma 14a4im 1536  a4ime 1538  spim 1537
[Tarski] p. 70Lemma 16ax-11 1331  ax-11o 1614  ax11i 1515
[Tarski] p. 70Lemmas 16 and 17sb6 1674
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1352
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax-13 1338  ax-14 1339
[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 2522
[WhiteheadRussell] p. 102Theorem *2.15con1dc 726
[WhiteheadRussell] p. 103Theorem *2.16con3 552
[WhiteheadRussell] p. 103Theorem *2.17ax-3 2512
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 2515  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 2532  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 2606
[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 2541  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 2526
[WhiteheadRussell] p. 117Theorem *4.13notnot 2523  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 1301
[WhiteheadRussell] p. 120Theorem *4.5anordc 825
[WhiteheadRussell] p. 120Theorem *4.6imor 2534  imordc 768
[WhiteheadRussell] p. 120Theorem *4.7anclb 300
[WhiteheadRussell] p. 120Theorem *4.51ianordc 770
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 2599
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 2600
[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 2601  pm4.57 2602
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 2603
[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 2604
[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 2605
[WhiteheadRussell] p. 121Theorem *4.79pm4.79dc 777
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 604
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 2598
[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 1215
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 715
[WhiteheadRussell] p. 124Theorem *5.17pm5.17dc 778
[WhiteheadRussell] p. 124Theorem *5.18nbbndc 1220  pm5.18dc 750
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 603
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 592
[WhiteheadRussell] p. 124Theorem *5.22xordc 1218
[WhiteheadRussell] p. 124Theorem *5.23dfbi3dc 1223
[WhiteheadRussell] p. 124Theorem *5.24pm5.24dc 1224
[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 1769
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1306
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1452
[WhiteheadRussell] p. 164Theorem *11.52nalexn 2613
[WhiteheadRussell] p. 164Theorem *11.512exnexn 2615
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1683
[WhiteheadRussell] p. 175Definition *14.02df-eu 1807
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2101
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2102
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2483
[WhiteheadRussell] p. 192Theorem *14.26eupick 2574  eupickbi 2577

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