Metamath Proof Explorer

Table of Contents - 20.19. Mathbox for Wolf Lammen

1. wl-section-prop
2. ax-luk1
3. ax-luk2
4. ax-luk3
5. 1. Bootstrapping
   1. wl-section-boot
   2. wl-luk-imim1i
   3. wl-luk-syl
   4. wl-luk-imtrid
   5. wl-luk-pm2.18d
   6. wl-luk-con4i
   7. wl-luk-pm2.24i
   8. wl-luk-a1i
   9. wl-luk-mpi
   10. wl-luk-imim2i
   11. wl-luk-imtrdi
   12. wl-luk-ax3
   13. wl-luk-ax1
   14. wl-luk-pm2.27
   15. wl-luk-com12
   16. wl-luk-pm2.21
   17. wl-luk-con1i
   18. wl-luk-ja
   19. wl-luk-imim2
   20. wl-luk-a1d
   21. wl-luk-ax2
   22. wl-luk-id
   23. wl-luk-notnotr
   24. wl-luk-pm2.04
6. Implication chains
   1. wl-section-impchain
   2. wl-impchain-mp-x
   3. wl-impchain-mp-0
   4. wl-impchain-mp-1
   5. wl-impchain-mp-2
   6. wl-impchain-com-1.x
   7. wl-impchain-com-1.1
   8. wl-impchain-com-1.2
   9. wl-impchain-com-1.3
   10. wl-impchain-com-1.4
   11. wl-impchain-com-n.m
   12. wl-impchain-com-2.3
   13. wl-impchain-com-2.4
   14. wl-impchain-com-3.2.1
   15. wl-impchain-a1-x
   16. wl-impchain-a1-1
   17. wl-impchain-a1-2
   18. wl-impchain-a1-3
7. Theorems around the conditional operator
   1. wl-ifp-ncond1
   2. wl-ifp-ncond2
   3. wl-ifpimpr
   4. wl-ifp4impr
8. Alternative development of hadd, cadd
   1. wl-df-3xor
   2. wl-df3xor2
   3. wl-df3xor3
   4. wl-3xortru
   5. wl-3xorfal
   6. wl-3xorbi
   7. wl-3xorbi2
   8. wl-3xorbi123d
   9. wl-3xorbi123i
   10. wl-3xorrot
   11. wl-3xorcoma
   12. wl-3xorcomb
   13. wl-3xornot1
   14. wl-3xornot
   15. wl-1xor
   16. wl-2xor
   17. wl-df-3mintru2
   18. wl-df2-3mintru2
   19. wl-df3-3mintru2
   20. wl-df4-3mintru2
   21. wl-1mintru1
   22. wl-1mintru2
   23. wl-2mintru1
   24. wl-2mintru2
   25. wl-df3maxtru1
9. An alternative axiom ~ ax-13
   1. ax-wl-13v
   2. wl-ax13lem1
10. Other stuff
    1. wl-mps
    2. wl-syls1
    3. wl-syls2
    4. wl-embant
    5. wl-orel12
    6. wl-cases2-dnf
    7. wl-cbvmotv
    8. wl-moteq
    9. wl-motae
    10. wl-moae
    11. wl-euae
    12. wl-nax6im
    13. wl-hbae1
    14. wl-naevhba1v
    15. wl-spae
    16. wl-speqv
    17. wl-19.8eqv
    18. wl-19.2reqv
    19. wl-nfalv
    20. wl-nfimf1
    21. wl-nfae1
    22. wl-nfnae1
    23. wl-aetr
    24. wl-axc11r
    25. wl-dral1d
    26. wl-cbvalnaed
    27. wl-cbvalnae
    28. wl-exeq
    29. wl-aleq
    30. wl-nfeqfb
    31. wl-nfs1t
    32. wl-equsalvw
    33. wl-equsald
    34. wl-equsal
    35. wl-equsal1t
    36. wl-equsalcom
    37. wl-equsal1i
    38. wl-sb6rft
    39. wl-cbvalsbi
    40. wl-sbrimt
    41. wl-sblimt
    42. wl-sb8t
    43. wl-sb8et
    44. wl-sbhbt
    45. wl-sbnf1
    46. wl-equsb3
    47. wl-equsb4
    48. wl-2sb6d
    49. wl-sbcom2d-lem1
    50. wl-sbcom2d-lem2
    51. wl-sbcom2d
    52. wl-sbalnae
    53. wl-sbal1
    54. wl-sbal2
    55. wl-2spsbbi
    56. wl-lem-exsb
    57. wl-lem-nexmo
    58. wl-lem-moexsb
    59. wl-alanbii
    60. wl-mo2df
    61. wl-mo2tf
    62. wl-eudf
    63. wl-eutf
    64. wl-euequf
    65. wl-mo2t
    66. wl-mo3t
    67. wl-sb8eut
    68. wl-sb8mot
    69. wl-axc11rc11
    70. ax-wl-11v
    71. wl-ax11-lem1
    72. wl-ax11-lem2
    73. wl-ax11-lem3
    74. wl-ax11-lem4
    75. wl-ax11-lem5
    76. wl-ax11-lem6
    77. wl-ax11-lem7
    78. wl-ax11-lem8
    79. wl-ax11-lem9
    80. wl-ax11-lem10
    81. wl-clabv
    82. wl-dfclab
    83. wl-clabtv
    84. wl-clabt