Metamath Proof Explorer


Table of Contents - 1.2. Propositional calculus

Propositional calculus deals with general truths about well-formed formulas (wffs) regardless of how they are constructed. The simplest propositional truth is , which can be read "if something is true, then it is true" - rather trivial and obvious, but nonetheless it must be proved from the axioms (see theorem id).

Our system of propositional calculus consists of three basic axioms and another axiom that defines the modus-ponens inference rule. It is attributed to Jan Lukasiewicz (pronounced woo-kah-SHAY-vitch) and was popularized by Alonzo Church, who called it system P2. (Thanks to Ted Ulrich for this information.) These axioms are ax-1, ax-2, ax-3, and (for modus ponens) ax-mp. Some closely followed texts include [Margaris] for the axioms and [WhiteheadRussell] for the theorems.

The propositional calculus used here is the classical system widely used by mathematicians. In particular, this logic system accepts the "law of the excluded middle" as proven in exmid, which says that a logical statement is either true or not true. This is an essential distinction of classical logic and is not a theorem of intuitionistic logic.

All 194 axioms, definitions, and theorems for propositional calculus in Principia Mathematica (specifically *1.2 through *5.75) are axioms or formally proven. See the Bibliographic Cross-References at mmbiblio.html for a complete cross-reference from sources used to its formalization in the Metamath Proof Explorer.

  1. Recursively define primitive wffs for propositional calculus
    1. wn
    2. wi
  2. The axioms of propositional calculus
    1. ax-mp
    2. ax-1
    3. ax-2
    4. ax-3
  3. Logical implication
    1. mp2
    2. mp2b
    3. a1i
    4. 2a1i
    5. mp1i
    6. a2i
    7. mpd
    8. imim2i
    9. syl
    10. 3syl
    11. 4syl
    12. mpi
    13. mpisyl
    14. id
    15. idALT
    16. idd
    17. a1d
    18. 2a1d
    19. a1i13
    20. 2a1
    21. a2d
    22. sylcom
    23. syl5com
    24. com12
    25. syl11
    26. syl5
    27. syl6
    28. syl56
    29. syl6com
    30. mpcom
    31. syli
    32. syl2im
    33. syl2imc
    34. pm2.27
    35. mpdd
    36. mpid
    37. mpdi
    38. mpii
    39. syld
    40. syldc
    41. mp2d
    42. a1dd
    43. 2a1dd
    44. pm2.43i
    45. pm2.43d
    46. pm2.43a
    47. pm2.43b
    48. pm2.43
    49. imim2d
    50. imim2
    51. embantd
    52. 3syld
    53. sylsyld
    54. imim12i
    55. imim1i
    56. imim3i
    57. sylc
    58. syl3c
    59. syl6mpi
    60. mpsyl
    61. mpsylsyld
    62. syl6c
    63. syl6ci
    64. syldd
    65. syl5d
    66. syl7
    67. syl6d
    68. syl8
    69. syl9
    70. syl9r
    71. syl10
    72. a1ddd
    73. imim12d
    74. imim1d
    75. imim1
    76. pm2.83
    77. peirceroll
    78. com23
    79. com3r
    80. com13
    81. com3l
    82. pm2.04
    83. com34
    84. com4l
    85. com4t
    86. com4r
    87. com24
    88. com14
    89. com45
    90. com35
    91. com25
    92. com5l
    93. com15
    94. com52l
    95. com52r
    96. com5r
    97. imim12
    98. jarr
    99. jarri
    100. pm2.86d
    101. pm2.86
    102. pm2.86i
    103. loolin
    104. loowoz
  4. 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
  5. Logical equivalence
    1. wb
    2. df-bi
    3. impbi
    4. impbii
    5. impbidd
    6. impbid21d
    7. impbid
    8. dfbi1
    9. dfbi1ALT
    10. biimp
    11. biimpi
    12. sylbi
    13. sylib
    14. sylbb
    15. biimpr
    16. bicom1
    17. bicom
    18. bicomd
    19. bicomi
    20. impbid1
    21. impbid2
    22. impcon4bid
    23. biimpri
    24. biimpd
    25. mpbi
    26. mpbir
    27. mpbid
    28. mpbii
    29. sylibr
    30. sylbir
    31. sylbbr
    32. sylbb1
    33. sylbb2
    34. sylibd
    35. sylbid
    36. mpbidi
    37. syl5bi
    38. syl5bir
    39. syl5ib
    40. syl5ibcom
    41. syl5ibr
    42. syl5ibrcom
    43. biimprd
    44. biimpcd
    45. biimprcd
    46. syl6ib
    47. syl6ibr
    48. syl6bi
    49. syl6bir
    50. syl7bi
    51. syl8ib
    52. mpbird
    53. mpbiri
    54. sylibrd
    55. sylbird
    56. biid
    57. biidd
    58. pm5.1im
    59. 2th
    60. 2thd
    61. monothetic
    62. ibi
    63. ibir
    64. ibd
    65. pm5.74
    66. pm5.74i
    67. pm5.74ri
    68. pm5.74d
    69. pm5.74rd
    70. bitri
    71. bitr2i
    72. bitr3i
    73. bitr4i
    74. bitrd
    75. bitr2d
    76. bitr3d
    77. bitr4d
    78. syl5bb
    79. syl5rbb
    80. bitr3id
    81. bitr3di
    82. syl6bb
    83. syl6rbb
    84. syl6bbr
    85. syl6rbbr
    86. 3imtr3i
    87. 3imtr4i
    88. 3imtr3d
    89. 3imtr4d
    90. 3imtr3g
    91. 3imtr4g
    92. 3bitri
    93. 3bitrri
    94. 3bitr2i
    95. 3bitr2ri
    96. 3bitr3i
    97. 3bitr3ri
    98. 3bitr4i
    99. 3bitr4ri
    100. 3bitrd
    101. 3bitrrd
    102. 3bitr2d
    103. 3bitr2rd
    104. 3bitr3d
    105. 3bitr3rd
    106. 3bitr4d
    107. 3bitr4rd
    108. 3bitr3g
    109. 3bitr4g
    110. notnotb
    111. con34b
    112. con4bid
    113. notbid
    114. notbi
    115. notbii
    116. con4bii
    117. mtbi
    118. mtbir
    119. mtbid
    120. mtbird
    121. mtbii
    122. mtbiri
    123. sylnib
    124. sylnibr
    125. sylnbi
    126. sylnbir
    127. xchnxbi
    128. xchnxbir
    129. xchbinx
    130. xchbinxr
    131. imbi2i
    132. jcndOLD
    133. bibi2i
    134. bibi1i
    135. bibi12i
    136. imbi2d
    137. imbi1d
    138. bibi2d
    139. bibi1d
    140. imbi12d
    141. bibi12d
    142. imbi12
    143. imbi1
    144. imbi2
    145. imbi1i
    146. imbi12i
    147. bibi1
    148. bitr3
    149. con2bi
    150. con2bid
    151. con1bid
    152. con1bii
    153. con2bii
    154. con1b
    155. con2b
    156. biimt
    157. pm5.5
    158. a1bi
    159. mt2bi
    160. mtt
    161. imnot
    162. pm5.501
    163. ibib
    164. ibibr
    165. tbt
    166. nbn2
    167. bibif
    168. nbn
    169. nbn3
    170. pm5.21im
    171. 2false
    172. 2falsed
    173. 2falsedOLD
    174. pm5.21ni
    175. pm5.21nii
    176. pm5.21ndd
    177. bija
    178. pm5.18
    179. xor3
    180. nbbn
    181. biass
    182. biluk
    183. pm5.19
    184. bi2.04
    185. pm5.4
    186. imdi
    187. pm5.41
    188. pm4.8
    189. pm4.81
    190. imim21b
  6. Logical conjunction
    1. wa
    2. df-an
    3. pm4.63
    4. pm4.67
    5. imnan
    6. imnani
    7. iman
    8. pm3.24
    9. annim
    10. pm4.61
    11. pm4.65
    12. imp
    13. impcom
    14. con3dimp
    15. mpnanrd
    16. impd
    17. impcomd
    18. ex
    19. expcom
    20. expdcom
    21. expd
    22. expcomd
    23. imp31
    24. imp32
    25. exp31
    26. exp32
    27. imp4b
    28. imp4a
    29. imp4c
    30. imp4d
    31. imp41
    32. imp42
    33. imp43
    34. imp44
    35. imp45
    36. exp4b
    37. exp4a
    38. exp4c
    39. exp4d
    40. exp41
    41. exp42
    42. exp43
    43. exp44
    44. exp45
    45. imp5d
    46. imp5a
    47. imp5g
    48. imp55
    49. imp511
    50. exp5c
    51. exp5j
    52. exp5l
    53. exp53
    54. pm3.3
    55. pm3.31
    56. impexp
    57. impancom
    58. expdimp
    59. expimpd
    60. impr
    61. impl
    62. expr
    63. expl
    64. ancoms
    65. pm3.22
    66. ancom
    67. ancomd
    68. biancomi
    69. biancomd
    70. ancomst
    71. ancomsd
    72. anasss
    73. anassrs
    74. anass
    75. pm3.2
    76. pm3.2i
    77. pm3.21
    78. pm3.43i
    79. pm3.43
    80. dfbi2
    81. dfbi
    82. biimpa
    83. biimpar
    84. biimpac
    85. biimparc
    86. adantr
    87. adantl
    88. simpl
    89. simpli
    90. simpr
    91. simpri
    92. intnan
    93. intnanr
    94. intnand
    95. intnanrd
    96. adantld
    97. adantrd
    98. pm3.41
    99. pm3.42
    100. simpld
    101. simprd
    102. simprbi
    103. simplbi
    104. simprbda
    105. simplbda
    106. simplbi2
    107. simplbi2comt
    108. simplbi2com
    109. simpl2im
    110. simplbiim
    111. impel
    112. mpan9
    113. sylan9
    114. sylan9r
    115. sylan9bb
    116. sylan9bbr
    117. jca
    118. jcad
    119. jca2
    120. jca31
    121. jca32
    122. jcai
    123. jcab
    124. pm4.76
    125. jctil
    126. jctir
    127. jccir
    128. jccil
    129. jctl
    130. jctr
    131. jctild
    132. jctird
    133. iba
    134. ibar
    135. biantru
    136. biantrur
    137. biantrud
    138. biantrurd
    139. bianfi
    140. bianfd
    141. baib
    142. baibr
    143. rbaibr
    144. rbaib
    145. baibd
    146. rbaibd
    147. bianabs
    148. pm5.44
    149. pm5.42
    150. ancl
    151. anclb
    152. ancr
    153. ancrb
    154. ancli
    155. ancri
    156. ancld
    157. ancrd
    158. impac
    159. anc2l
    160. anc2r
    161. anc2li
    162. anc2ri
    163. pm4.71
    164. pm4.71r
    165. pm4.71i
    166. pm4.71ri
    167. pm4.71d
    168. pm4.71rd
    169. pm4.24
    170. anidm
    171. anidmdbi
    172. anidms
    173. imdistan
    174. imdistani
    175. imdistanri
    176. imdistand
    177. imdistanda
    178. pm5.3
    179. pm5.32
    180. pm5.32i
    181. pm5.32ri
    182. pm5.32d
    183. pm5.32rd
    184. pm5.32da
    185. sylan
    186. sylanb
    187. sylanbr
    188. sylanbrc
    189. syl2anc
    190. syl2anc2
    191. sylancl
    192. sylancr
    193. sylancom
    194. sylanblc
    195. sylanblrc
    196. syldan
    197. sylan2
    198. sylan2b
    199. sylan2br
    200. syl2an
    201. syl2anr
    202. syl2anb
    203. syl2anbr
    204. sylancb
    205. sylancbr
    206. syldanl
    207. syland
    208. sylani
    209. sylan2d
    210. sylan2i
    211. syl2ani
    212. syl2and
    213. anim12d
    214. anim12d1
    215. anim1d
    216. anim2d
    217. anim12i
    218. anim12ci
    219. anim1i
    220. anim1ci
    221. anim2i
    222. anim12ii
    223. anim12dan
    224. im2anan9
    225. im2anan9r
    226. pm3.45
    227. anbi2i
    228. anbi1i
    229. anbi2ci
    230. anbi1ci
    231. anbi12i
    232. anbi12ci
    233. anbi2d
    234. anbi1d
    235. anbi12d
    236. anbi1
    237. anbi2
    238. anbi1cd
    239. pm4.38
    240. bi2anan9
    241. bi2anan9r
    242. bi2bian9
    243. bianass
    244. bianassc
    245. an21
    246. an12
    247. an32
    248. an13
    249. an31
    250. an12s
    251. ancom2s
    252. an13s
    253. an32s
    254. ancom1s
    255. an31s
    256. anass1rs
    257. an4
    258. an42
    259. an43
    260. an3
    261. an4s
    262. an42s
    263. anabs1
    264. anabs5
    265. anabs7
    266. anabsan
    267. anabss1
    268. anabss4
    269. anabss5
    270. anabsi5
    271. anabsi6
    272. anabsi7
    273. anabsi8
    274. anabss7
    275. anabsan2
    276. anabss3
    277. anandi
    278. anandir
    279. anandis
    280. anandirs
    281. sylanl1
    282. sylanl2
    283. sylanr1
    284. sylanr2
    285. syl6an
    286. syl2an2r
    287. syl2an2
    288. mpdan
    289. mpancom
    290. mpidan
    291. mpan
    292. mpan2
    293. mp2an
    294. mp4an
    295. mpan2d
    296. mpand
    297. mpani
    298. mpan2i
    299. mp2ani
    300. mp2and
    301. mpanl1
    302. mpanl2
    303. mpanl12
    304. mpanr1
    305. mpanr2
    306. mpanr12
    307. mpanlr1
    308. mpbirand
    309. mpbiran2d
    310. mpbiran
    311. mpbiran2
    312. mpbir2an
    313. mpbi2and
    314. mpbir2and
    315. adantll
    316. adantlr
    317. adantrl
    318. adantrr
    319. adantlll
    320. adantllr
    321. adantlrl
    322. adantlrr
    323. adantrll
    324. adantrlr
    325. adantrrl
    326. adantrrr
    327. ad2antrr
    328. ad2antlr
    329. ad2antrl
    330. ad2antll
    331. ad3antrrr
    332. ad3antlr
    333. ad4antr
    334. ad4antlr
    335. ad5antr
    336. ad5antlr
    337. ad6antr
    338. ad6antlr
    339. ad7antr
    340. ad7antlr
    341. ad8antr
    342. ad8antlr
    343. ad9antr
    344. ad9antlr
    345. ad10antr
    346. ad10antlr
    347. ad2ant2l
    348. ad2ant2r
    349. ad2ant2lr
    350. ad2ant2rl
    351. adantl3r
    352. ad4ant13
    353. ad4ant14
    354. ad4ant23
    355. ad4ant24
    356. adantl4r
    357. ad5ant12
    358. ad5ant13
    359. ad5ant14
    360. ad5ant15
    361. ad5ant23
    362. ad5ant24
    363. ad5ant25
    364. adantl5r
    365. adantl6r
    366. pm3.33
    367. pm3.34
    368. simpll
    369. simplld
    370. simplr
    371. simplrd
    372. simprl
    373. simprld
    374. simprr
    375. simprrd
    376. simplll
    377. simpllr
    378. simplrl
    379. simplrr
    380. simprll
    381. simprlr
    382. simprrl
    383. simprrr
    384. simp-4l
    385. simp-4r
    386. simp-5l
    387. simp-5r
    388. simp-6l
    389. simp-6r
    390. simp-7l
    391. simp-7r
    392. simp-8l
    393. simp-8r
    394. simp-9l
    395. simp-9r
    396. simp-10l
    397. simp-10r
    398. simp-11l
    399. simp-11r
    400. pm2.01da
    401. pm2.18da
    402. impbida
    403. pm5.21nd
    404. pm3.35
    405. pm5.74da
    406. bitr
    407. biantr
    408. pm4.14
    409. pm3.37
    410. anim12
    411. pm3.4
    412. exbiri
    413. pm2.61ian
    414. pm2.61dan
    415. pm2.61ddan
    416. pm2.61dda
    417. mtand
    418. pm2.65da
    419. condan
    420. biadan
    421. biadani
    422. biadaniALT
    423. biadanii
    424. pm5.1
    425. pm5.21
    426. pm5.35
    427. abai
    428. pm4.45im
    429. impimprbi
    430. nan
    431. pm5.31
    432. pm5.31r
    433. pm4.15
    434. pm5.36
    435. annotanannot
    436. pm5.33
    437. syl12anc
    438. syl21anc
    439. syl22anc
    440. syl1111anc
    441. mpsyl4anc
    442. pm4.87
    443. bimsc1
    444. a2and
    445. animpimp2impd
  7. Logical disjunction
    1. wo
    2. df-or
    3. pm4.64
    4. pm4.66
    5. pm2.53
    6. pm2.54
    7. imor
    8. imori
    9. imorri
    10. pm4.62
    11. jaoi
    12. jao1i
    13. jaod
    14. mpjaod
    15. ori
    16. orri
    17. orrd
    18. ord
    19. orci
    20. olci
    21. orc
    22. olc
    23. pm1.4
    24. orcom
    25. orcomd
    26. orcoms
    27. orcd
    28. olcd
    29. orcs
    30. olcs
    31. olcnd
    32. unitreslOLD
    33. orcnd
    34. mtord
    35. pm3.2ni
    36. pm2.45
    37. pm2.46
    38. pm2.47
    39. pm2.48
    40. pm2.49
    41. norbi
    42. nbior
    43. orel1
    44. pm2.25
    45. orel2
    46. pm2.67-2
    47. pm2.67
    48. curryax
    49. exmid
    50. exmidd
    51. pm2.1
    52. pm2.13
    53. pm2.621
    54. pm2.62
    55. pm2.68
    56. dfor2
    57. pm2.07
    58. pm1.2
    59. oridm
    60. pm4.25
    61. pm2.4
    62. pm2.41
    63. orim12i
    64. orim1i
    65. orim2i
    66. orim12dALT
    67. orbi2i
    68. orbi1i
    69. orbi12i
    70. orbi2d
    71. orbi1d
    72. orbi1
    73. orbi12d
    74. pm1.5
    75. or12
    76. orass
    77. pm2.31
    78. pm2.32
    79. pm2.3
    80. or32
    81. or4
    82. or42
    83. orordi
    84. orordir
    85. orimdi
    86. pm2.76
    87. pm2.85
    88. pm2.75
    89. pm4.78
    90. biort
    91. biorf
    92. biortn
    93. biorfi
    94. pm2.26
    95. pm2.63
    96. pm2.64
    97. pm2.42
    98. pm5.11g
    99. pm5.11
    100. pm5.12
    101. pm5.14
    102. pm5.13
    103. pm5.55
    104. pm4.72
    105. imimorb
    106. oibabs
    107. orbidi
    108. pm5.7
  8. Mixed connectives
    1. jaao
    2. jaoa
    3. jaoian
    4. jaodan
    5. mpjaodan
    6. pm3.44
    7. jao
    8. jaob
    9. pm4.77
    10. pm3.48
    11. orim12d
    12. orim1d
    13. orim2d
    14. orim2
    15. pm2.38
    16. pm2.36
    17. pm2.37
    18. pm2.81
    19. pm2.8
    20. pm2.73
    21. pm2.74
    22. pm2.82
    23. pm4.39
    24. animorl
    25. animorr
    26. animorlr
    27. animorrl
    28. ianor
    29. anor
    30. ioran
    31. pm4.52
    32. pm4.53
    33. pm4.54
    34. pm4.55
    35. pm4.56
    36. oran
    37. pm4.57
    38. pm3.1
    39. pm3.11
    40. pm3.12
    41. pm3.13
    42. pm3.14
    43. pm4.44
    44. pm4.45
    45. orabs
    46. oranabs
    47. pm5.61
    48. pm5.6
    49. orcanai
    50. pm4.79
    51. pm5.53
    52. ordi
    53. ordir
    54. andi
    55. andir
    56. orddi
    57. anddi
    58. pm5.17
    59. pm5.15
    60. pm5.16
    61. xor
    62. nbi2
    63. xordi
    64. pm5.54
    65. pm5.62
    66. pm5.63
    67. niabn
    68. ninba
    69. pm4.43
    70. pm4.82
    71. pm4.83
    72. pclem6
    73. bigolden
    74. pm5.71
    75. pm5.75
    76. ecase2d
    77. ecase3
    78. ecase
    79. ecase3d
    80. ecased
    81. ecase3ad
    82. ccase
    83. ccased
    84. ccase2
    85. 4cases
    86. 4casesdan
    87. cases
    88. dedlem0a
    89. dedlem0b
    90. dedlema
    91. dedlemb
    92. cases2
    93. cases2ALT
    94. dfbi3
    95. pm5.24
    96. 4exmid
    97. consensus
    98. pm4.42
    99. prlem1
    100. prlem2
    101. oplem1
    102. dn1
    103. bianir
    104. jaoi2
    105. jaoi3
    106. ornld
  9. The conditional operator for propositions
    1. wif
    2. df-ifp
    3. dfifp2
    4. dfifp3
    5. dfifp4
    6. dfifp5
    7. dfifp6
    8. dfifp7
    9. ifpdfbi
    10. anifp
    11. ifpor
    12. ifpn
    13. ifpnOLD
    14. ifptru
    15. ifpfal
    16. ifpid
    17. casesifp
    18. ifpbi123d
    19. ifpbi123dOLD
    20. ifpbi23d
    21. ifpimpda
    22. 1fpid3
  10. The weak deduction theorem for propositional calculus
    1. elimh
    2. dedt
    3. con3ALT
  11. Abbreviated conjunction and disjunction of three wff's
    1. w3o
    2. w3a
    3. df-3or
    4. df-3an
    5. 3orass
    6. 3orel1
    7. 3orrot
    8. 3orcoma
    9. 3orcomb
    10. 3anass
    11. 3anan12
    12. 3anan32
    13. 3ancoma
    14. 3ancomb
    15. 3anrot
    16. 3anrev
    17. anandi3
    18. anandi3r
    19. 3anidm
    20. 3an4anass
    21. 3ioran
    22. 3ianor
    23. 3anor
    24. 3oran
    25. 3impa
    26. 3imp
    27. 3imp31
    28. 3imp231
    29. 3imp21
    30. 3impb
    31. 3impib
    32. 3impia
    33. 3expa
    34. 3exp
    35. 3expb
    36. 3expia
    37. 3expib
    38. 3com12
    39. 3com13
    40. 3comr
    41. 3com23
    42. 3coml
    43. 3jca
    44. 3jcad
    45. 3adant1
    46. 3adant2
    47. 3adant3
    48. 3ad2ant1
    49. 3ad2ant2
    50. 3ad2ant3
    51. simp1
    52. simp2
    53. simp3
    54. simp1i
    55. simp2i
    56. simp3i
    57. simp1d
    58. simp2d
    59. simp3d
    60. simp1bi
    61. simp2bi
    62. simp3bi
    63. 3simpa
    64. 3simpb
    65. 3simpc
    66. 3anim123i
    67. 3anim1i
    68. 3anim2i
    69. 3anim3i
    70. 3anbi123i
    71. 3orbi123i
    72. 3anbi1i
    73. 3anbi2i
    74. 3anbi3i
    75. syl3an
    76. syl3anb
    77. syl3anbr
    78. syl3an1
    79. syl3an2
    80. syl3an3
    81. 3adantl1
    82. 3adantl2
    83. 3adantl3
    84. 3adantr1
    85. 3adantr2
    86. 3adantr3
    87. ad4ant123
    88. ad4ant124
    89. ad4ant134
    90. ad4ant234
    91. 3adant1l
    92. 3adant1r
    93. 3adant2l
    94. 3adant2r
    95. 3adant3l
    96. 3adant3r
    97. 3adant3r1
    98. 3adant3r2
    99. 3adant3r3
    100. 3ad2antl1
    101. 3ad2antl2
    102. 3ad2antl3
    103. 3ad2antr1
    104. 3ad2antr2
    105. 3ad2antr3
    106. simpl1
    107. simpl2
    108. simpl3
    109. simpr1
    110. simpr2
    111. simpr3
    112. simp1l
    113. simp1r
    114. simp2l
    115. simp2r
    116. simp3l
    117. simp3r
    118. simp11
    119. simp12
    120. simp13
    121. simp21
    122. simp22
    123. simp23
    124. simp31
    125. simp32
    126. simp33
    127. simpll1
    128. simpll2
    129. simpll3
    130. simplr1
    131. simplr2
    132. simplr3
    133. simprl1
    134. simprl2
    135. simprl3
    136. simprr1
    137. simprr2
    138. simprr3
    139. simpl1l
    140. simpl1r
    141. simpl2l
    142. simpl2r
    143. simpl3l
    144. simpl3r
    145. simpr1l
    146. simpr1r
    147. simpr2l
    148. simpr2r
    149. simpr3l
    150. simpr3r
    151. simp1ll
    152. simp1lr
    153. simp1rl
    154. simp1rr
    155. simp2ll
    156. simp2lr
    157. simp2rl
    158. simp2rr
    159. simp3ll
    160. simp3lr
    161. simp3rl
    162. simp3rr
    163. simpl11
    164. simpl12
    165. simpl13
    166. simpl21
    167. simpl22
    168. simpl23
    169. simpl31
    170. simpl32
    171. simpl33
    172. simpr11
    173. simpr12
    174. simpr13
    175. simpr21
    176. simpr22
    177. simpr23
    178. simpr31
    179. simpr32
    180. simpr33
    181. simp1l1
    182. simp1l2
    183. simp1l3
    184. simp1r1
    185. simp1r2
    186. simp1r3
    187. simp2l1
    188. simp2l2
    189. simp2l3
    190. simp2r1
    191. simp2r2
    192. simp2r3
    193. simp3l1
    194. simp3l2
    195. simp3l3
    196. simp3r1
    197. simp3r2
    198. simp3r3
    199. simp11l
    200. simp11r
    201. simp12l
    202. simp12r
    203. simp13l
    204. simp13r
    205. simp21l
    206. simp21r
    207. simp22l
    208. simp22r
    209. simp23l
    210. simp23r
    211. simp31l
    212. simp31r
    213. simp32l
    214. simp32r
    215. simp33l
    216. simp33r
    217. simp111
    218. simp112
    219. simp113
    220. simp121
    221. simp122
    222. simp123
    223. simp131
    224. simp132
    225. simp133
    226. simp211
    227. simp212
    228. simp213
    229. simp221
    230. simp222
    231. simp223
    232. simp231
    233. simp232
    234. simp233
    235. simp311
    236. simp312
    237. simp313
    238. simp321
    239. simp322
    240. simp323
    241. simp331
    242. simp332
    243. simp333
    244. 3anibar
    245. 3mix1
    246. 3mix2
    247. 3mix3
    248. 3mix1i
    249. 3mix2i
    250. 3mix3i
    251. 3mix1d
    252. 3mix2d
    253. 3mix3d
    254. 3pm3.2i
    255. pm3.2an3
    256. mpbir3an
    257. mpbir3and
    258. syl3anbrc
    259. syl21anbrc
    260. 3imp3i2an
    261. ex3
    262. 3imp1
    263. 3impd
    264. 3imp2
    265. 3impdi
    266. 3impdir
    267. 3exp1
    268. 3expd
    269. 3exp2
    270. exp5o
    271. exp516
    272. exp520
    273. 3impexp
    274. 3an1rs
    275. 3anassrs
    276. ad5ant245
    277. ad5ant234
    278. ad5ant235
    279. ad5ant123
    280. ad5ant124
    281. ad5ant125
    282. ad5ant134
    283. ad5ant135
    284. ad5ant145
    285. ad5ant2345
    286. syl3anc
    287. syl13anc
    288. syl31anc
    289. syl112anc
    290. syl121anc
    291. syl211anc
    292. syl23anc
    293. syl32anc
    294. syl122anc
    295. syl212anc
    296. syl221anc
    297. syl113anc
    298. syl131anc
    299. syl311anc
    300. syl33anc
    301. syl222anc
    302. syl123anc
    303. syl132anc
    304. syl213anc
    305. syl231anc
    306. syl312anc
    307. syl321anc
    308. syl133anc
    309. syl313anc
    310. syl331anc
    311. syl223anc
    312. syl232anc
    313. syl322anc
    314. syl233anc
    315. syl323anc
    316. syl332anc
    317. syl333anc
    318. syl3an1b
    319. syl3an2b
    320. syl3an3b
    321. syl3an1br
    322. syl3an2br
    323. syl3an3br
    324. syld3an3
    325. syld3an1
    326. syld3an2
    327. syl3anl1
    328. syl3anl2
    329. syl3anl3
    330. syl3anl
    331. syl3anr1
    332. syl3anr2
    333. syl3anr3
    334. 3anidm12
    335. 3anidm13
    336. 3anidm23
    337. syl2an3an
    338. syl2an23an
    339. 3ori
    340. 3jao
    341. 3jaob
    342. 3jaoi
    343. 3jaod
    344. 3jaoian
    345. 3jaodan
    346. mpjao3dan
    347. mpjao3danOLD
    348. 3jaao
    349. syl3an9b
    350. 3orbi123d
    351. 3anbi123d
    352. 3anbi12d
    353. 3anbi13d
    354. 3anbi23d
    355. 3anbi1d
    356. 3anbi2d
    357. 3anbi3d
    358. 3anim123d
    359. 3orim123d
    360. an6
    361. 3an6
    362. 3or6
    363. mp3an1
    364. mp3an2
    365. mp3an3
    366. mp3an12
    367. mp3an13
    368. mp3an23
    369. mp3an1i
    370. mp3anl1
    371. mp3anl2
    372. mp3anl3
    373. mp3anr1
    374. mp3anr2
    375. mp3anr3
    376. mp3an
    377. mpd3an3
    378. mpd3an23
    379. mp3and
    380. mp3an12i
    381. mp3an2i
    382. mp3an3an
    383. mp3an2ani
    384. biimp3a
    385. biimp3ar
    386. 3anandis
    387. 3anandirs
    388. ecase23d
    389. 3ecase
    390. 3bior1fd
    391. 3bior1fand
    392. 3bior2fd
    393. 3biant1d
    394. intn3an1d
    395. intn3an2d
    396. intn3an3d
    397. an3andi
    398. an33rean
    399. an33reanOLD
  12. Logical "nand" (Sheffer stroke)
    1. wnan
    2. df-nan
    3. nanan
    4. nanimn
    5. nanor
    6. nancom
    7. nannan
    8. nanim
    9. nannot
    10. nanbi
    11. nanbi1
    12. nanbi2
    13. nanbi12
    14. nanbi1i
    15. nanbi2i
    16. nanbi12i
    17. nanbi1d
    18. nanbi2d
    19. nanbi12d
    20. nanass
  13. Logical "xor"
    1. wxo
    2. df-xor
    3. xnor
    4. xorcom
    5. xorcomOLD
    6. xorass
    7. excxor
    8. xor2
    9. xoror
    10. xornan
    11. xornan2
    12. xorneg2
    13. xorneg1
    14. xorneg
    15. xorbi12i
    16. xorbi12iOLD
    17. xorbi12d
    18. anxordi
    19. xorexmid
  14. Logical "nor"
    1. wnor
    2. df-nor
    3. norcom
    4. norcomOLD
    5. nornot
    6. nornotOLD
    7. noran
    8. noranOLD
    9. noror
    10. nororOLD
    11. norasslem1
    12. norasslem2
    13. norasslem3
    14. norass
    15. norassOLD
  15. True and false constants
    1. Universal quantifier for use by df-tru
    2. Equality predicate for use by df-tru
    3. The true constant
    4. The false constant
  16. Truth tables
    1. Implication
    2. Negation
    3. Equivalence
    4. Conjunction
    5. Disjunction
    6. Alternative denial
    7. Exclusive disjunction
    8. Joint denial
  17. Half adder and full adder in propositional calculus
    1. Full adder: sum
    2. Full adder: carry