Metamath Proof Explorer

Table of Contents - 20.22.1. Tools for automatic proof building

The results in this section are mostly meant for being used by automatic proof building programs. As a result, they might appear less useful or meaningful than others to human beings.

1. efald2
2. notbinot1
3. bicontr
4. impor
5. orfa
6. notbinot2
7. biimpor
8. orfa1
9. orfa2
10. bifald
11. orsild
12. orsird
13. cnf1dd
14. cnf2dd
15. cnfn1dd
16. cnfn2dd
17. or32dd
18. notornotel1
19. notornotel2
20. contrd
21. an12i
22. exmid2
23. selconj
24. truconj
25. orel
26. negel
27. botel
28. tradd
29. gm-sbtru
30. sbfal
31. sbcani
32. sbcori
33. sbcimi
34. sbcni
35. sbali
36. sbexi
37. sbcalf
38. sbcexf
39. sbcalfi
40. sbcexfi
41. spsbcdi
42. alrimii
43. spesbcdi
44. exlimddvf
45. exlimddvfi
46. sbceq1ddi
47. sbccom2lem
48. sbccom2
49. sbccom2f
50. sbccom2fi
51. csbcom2fi