Metamath Proof Explorer


Table of Contents - 1.2.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
  400. 3orel2
  401. 3orel3