Metamath Proof Explorer

Table of Contents - 1.3.6. Derive the Lukasiewicz axioms from Nicod's axiom

1. nic-imp
2. nic-idlem1
3. nic-idlem2
4. nic-id
5. nic-swap
6. nic-isw1
7. nic-isw2
8. nic-iimp1
9. nic-iimp2
10. nic-idel
11. nic-ich
12. nic-idbl
13. nic-bijust
14. nic-bi1
15. nic-bi2
16. nic-stdmp
17. nic-luk1
18. nic-luk2
19. nic-luk3