Metamath Proof Explorer

Table of Contents - 20.22. Mathbox for Giovanni Mascellani

1. Tools for automatic proof building
   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
2. Tseitin axioms
   1. fald
   2. tsim1
   3. tsim2
   4. tsim3
   5. tsbi1
   6. tsbi2
   7. tsbi3
   8. tsbi4
   9. tsxo1
   10. tsxo2
   11. tsxo3
   12. tsxo4
   13. tsan1
   14. tsan2
   15. tsan3
   16. tsna1
   17. tsna2
   18. tsna3
   19. tsor1
   20. tsor2
   21. tsor3
   22. ts3an1
   23. ts3an2
   24. ts3an3
   25. ts3or1
   26. ts3or2
   27. ts3or3
3. Equality deductions
   1. iuneq2f
   2. rabeq12f
   3. csbeq12
   4. sbeqi
   5. ralbi12f
   6. oprabbi
   7. mpobi123f
   8. iuneq12f
   9. iineq12f
   10. opabbi
   11. mptbi12f
4. Miscellanea
   1. orcomdd
   2. scottexf
   3. scott0f
   4. scottn0f
   5. ac6s3f
   6. ac6s6
   7. ac6s6f