Metamath Proof Explorer
Table of Contents - 21.24.2. Tseitin axioms
A collection of Tseitin axioms used to convert a wff to Conjunctive
Normal Form.
- fald
- tsim1
- tsim2
- tsim3
- tsbi1
- tsbi2
- tsbi3
- tsbi4
- tsxo1
- tsxo2
- tsxo3
- tsxo4
- tsan1
- tsan2
- tsan3
- tsna1
- tsna2
- tsna3
- tsor1
- tsor2
- tsor3
- ts3an1
- ts3an2
- ts3an3
- ts3or1
- ts3or2
- ts3or3