Metamath Proof Explorer

Table of Contents - 1.3.8. Derive the Lukasiewicz Axioms from the Tarski-Bernays-Wajsberg Axioms

1. tbw-bijust
2. tbw-negdf
3. tbw-ax1
4. tbw-ax2
5. tbw-ax3
6. tbw-ax4
7. tbwsyl
8. tbwlem1
9. tbwlem2
10. tbwlem3
11. tbwlem4
12. tbwlem5
13. re1luk1
14. re1luk2
15. re1luk3