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. impt
67. pm2.61d
68. pm2.61d1
69. pm2.61d2
70. pm2.61i
71. pm2.61ii
72. pm2.61nii
73. pm2.61iii
74. ja
75. jad
76. pm2.01
77. pm2.01d
78. pm2.6
79. pm2.61
80. pm2.65
81. pm2.65i
82. pm2.21dd
83. pm2.65d
84. mto
85. mtod
86. mtoi
87. mt2
88. mt3
89. peirce
90. looinv
91. bijust0
92. bijust