Metamath Proof Explorer


Table of Contents - 1.2.6. Logical conjunction

This section defines conjunction of two formulas, denoted by infix "" and read "and". It is defined in terms of implication and negation, which is possible in classical logic (but not in intuitionistic logic: see iset.mm).

After the definition, we briefly introduce conversion of simple expressions to and from conjunction. Two simple operations called importation (imp) and exportation (ex) follow. In the propositions-as-types interpretation, they correspond to uncurrying and currying respectively. They are foundational for this section. Most of the theorems proved here trace back to them, mostly indirectly, in a layered fashion, where more complex expressions are built from simpler ones. Here are some of these successive layers: importation and exportation, commutativity and associativity laws, adding antecedents and simplifying, conjunction of consequents, syllogisms, etc.

As indicated in the "note on definitions" in the section comment for logical equivalence, some theorems containing only implication, negation and conjunction are placed in the section after disjunction since theirs proofs use disjunction (although this is not required since definitions are conservative, see said section comment).

  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. sylbida
  198. sylan2
  199. sylan2b
  200. sylan2br
  201. syl2an
  202. syl2anr
  203. syl2anb
  204. syl2anbr
  205. sylancb
  206. sylancbr
  207. syldanl
  208. syland
  209. sylani
  210. sylan2d
  211. sylan2i
  212. syl2ani
  213. syl2and
  214. anim12d
  215. anim12d1
  216. anim1d
  217. anim2d
  218. anim12i
  219. anim12ci
  220. anim1i
  221. anim1ci
  222. anim2i
  223. anim12ii
  224. anim12dan
  225. im2anan9
  226. im2anan9r
  227. pm3.45
  228. anbi2i
  229. anbi1i
  230. anbi2ci
  231. anbi1ci
  232. anbi12i
  233. anbi12ci
  234. anbi2d
  235. anbi1d
  236. anbi12d
  237. anbi1
  238. anbi2
  239. anbi1cd
  240. pm4.38
  241. bi2anan9
  242. bi2anan9r
  243. bi2bian9
  244. bianass
  245. bianassc
  246. an21
  247. an12
  248. an32
  249. an13
  250. an31
  251. an12s
  252. ancom2s
  253. an13s
  254. an32s
  255. ancom1s
  256. an31s
  257. anass1rs
  258. an4
  259. an42
  260. an43
  261. an3
  262. an4s
  263. an42s
  264. anabs1
  265. anabs5
  266. anabs7
  267. anabsan
  268. anabss1
  269. anabss4
  270. anabss5
  271. anabsi5
  272. anabsi6
  273. anabsi7
  274. anabsi8
  275. anabss7
  276. anabsan2
  277. anabss3
  278. anandi
  279. anandir
  280. anandis
  281. anandirs
  282. sylanl1
  283. sylanl2
  284. sylanr1
  285. sylanr2
  286. syl6an
  287. syl2an2r
  288. syl2an2
  289. mpdan
  290. mpancom
  291. mpidan
  292. mpan
  293. mpan2
  294. mp2an
  295. mp4an
  296. mpan2d
  297. mpand
  298. mpani
  299. mpan2i
  300. mp2ani
  301. mp2and
  302. mpanl1
  303. mpanl2
  304. mpanl12
  305. mpanr1
  306. mpanr2
  307. mpanr12
  308. mpanlr1
  309. mpbirand
  310. mpbiran2d
  311. mpbiran
  312. mpbiran2
  313. mpbir2an
  314. mpbi2and
  315. mpbir2and
  316. adantll
  317. adantlr
  318. adantrl
  319. adantrr
  320. adantlll
  321. adantllr
  322. adantlrl
  323. adantlrr
  324. adantrll
  325. adantrlr
  326. adantrrl
  327. adantrrr
  328. ad2antrr
  329. ad2antlr
  330. ad2antrl
  331. ad2antll
  332. ad3antrrr
  333. ad3antlr
  334. ad4antr
  335. ad4antlr
  336. ad5antr
  337. ad5antlr
  338. ad6antr
  339. ad6antlr
  340. ad7antr
  341. ad7antlr
  342. ad8antr
  343. ad8antlr
  344. ad9antr
  345. ad9antlr
  346. ad10antr
  347. ad10antlr
  348. ad2ant2l
  349. ad2ant2r
  350. ad2ant2lr
  351. ad2ant2rl
  352. adantl3r
  353. ad4ant13
  354. ad4ant14
  355. ad4ant23
  356. ad4ant24
  357. adantl4r
  358. ad5ant12
  359. ad5ant13
  360. ad5ant14
  361. ad5ant15
  362. ad5ant23
  363. ad5ant24
  364. ad5ant25
  365. adantl5r
  366. adantl6r
  367. pm3.33
  368. pm3.34
  369. simpll
  370. simplld
  371. simplr
  372. simplrd
  373. simprl
  374. simprld
  375. simprr
  376. simprrd
  377. simplll
  378. simpllr
  379. simplrl
  380. simplrr
  381. simprll
  382. simprlr
  383. simprrl
  384. simprrr
  385. simp-4l
  386. simp-4r
  387. simp-5l
  388. simp-5r
  389. simp-6l
  390. simp-6r
  391. simp-7l
  392. simp-7r
  393. simp-8l
  394. simp-8r
  395. simp-9l
  396. simp-9r
  397. simp-10l
  398. simp-10r
  399. simp-11l
  400. simp-11r
  401. pm2.01da
  402. pm2.18da
  403. impbida
  404. pm5.21nd
  405. pm3.35
  406. pm5.74da
  407. bitr
  408. biantr
  409. pm4.14
  410. pm3.37
  411. anim12
  412. pm3.4
  413. exbiri
  414. pm2.61ian
  415. pm2.61dan
  416. pm2.61ddan
  417. pm2.61dda
  418. mtand
  419. pm2.65da
  420. condan
  421. biadan
  422. biadani
  423. biadaniALT
  424. biadanii
  425. biadanid
  426. pm5.1
  427. pm5.21
  428. pm5.35
  429. abai
  430. pm4.45im
  431. impimprbi
  432. nan
  433. pm5.31
  434. pm5.31r
  435. pm4.15
  436. pm5.36
  437. annotanannot
  438. pm5.33
  439. syl12anc
  440. syl21anc
  441. syl22anc
  442. syl1111anc
  443. syldbl2
  444. mpsyl4anc
  445. pm4.87
  446. bimsc1
  447. a2and
  448. animpimp2impd