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. nsyl5
  51. pm3.2im
  52. jc
  53. jcn
  54. jcnd
  55. impi
  56. expi
  57. simprim
  58. simplim
  59. pm2.5g
  60. pm2.5
  61. conax1
  62. conax1k
  63. pm2.51
  64. pm2.52
  65. pm2.521g
  66. pm2.521g2
  67. pm2.521
  68. expt
  69. impt
  70. pm2.61d
  71. pm2.61d1
  72. pm2.61d2
  73. pm2.61i
  74. pm2.61ii
  75. pm2.61nii
  76. pm2.61iii
  77. ja
  78. jad
  79. pm2.61iOLD
  80. pm2.01
  81. pm2.01d
  82. pm2.6
  83. pm2.61
  84. pm2.65
  85. pm2.65i
  86. pm2.21dd
  87. pm2.65d
  88. mto
  89. mtod
  90. mtoi
  91. mt2
  92. mt3
  93. peirce
  94. looinv
  95. bijust0
  96. bijust