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