Metamath Proof Explorer

Table of Contents - 1.2.4. Logical negation

This section makes our first use of the third axiom of propositional calculus, ax-3. It introduces logical negation.

  1. con4
  2. con4i
  3. con4d
  4. mt4
  5. mt4d
  6. mt4i
  7. pm2.21i
  8. pm2.24ii
  9. pm2.21d
  10. pm2.21ddALT
  11. pm2.21
  12. pm2.24
  13. jarl
  14. jarli
  15. pm2.18d
  16. pm2.18
  17. pm2.18OLD
  18. pm2.18dOLD
  19. pm2.18i
  20. notnotr
  21. notnotri
  22. notnotriALT
  23. notnotrd
  24. con2d
  25. con2
  26. mt2d
  27. mt2i
  28. nsyl3
  29. con2i
  30. nsyl
  31. nsyl2
  32. notnot
  33. notnoti
  34. notnotd
  35. con1d
  36. con1
  37. con1i
  38. mt3d
  39. mt3i
  40. nsyl2OLD
  41. pm2.24i
  42. pm2.24d
  43. con3d
  44. con3
  45. con3i
  46. con3rr3
  47. nsyld
  48. nsyli
  49. nsyl4
  50. pm3.2im
  51. jc
  52. jcn
  53. jcnd
  54. impi
  55. expi
  56. simprim
  57. simplim
  58. pm2.5g
  59. pm2.5
  60. conax1
  61. conax1k
  62. pm2.51
  63. pm2.52
  64. pm2.521g
  65. pm2.521g2
  66. pm2.521
  67. expt
  68. impt
  69. pm2.61d
  70. pm2.61d1
  71. pm2.61d2
  72. pm2.61i
  73. pm2.61ii
  74. pm2.61nii
  75. pm2.61iii
  76. ja
  77. jad
  78. pm2.61iOLD
  79. pm2.01
  80. pm2.01d
  81. pm2.6
  82. pm2.61
  83. pm2.65
  84. pm2.65i
  85. pm2.21dd
  86. pm2.65d
  87. mto
  88. mtod
  89. mtoi
  90. mt2
  91. mt3
  92. peirce
  93. looinv
  94. bijust0
  95. bijust