Metamath Proof Explorer

Table of Contents - 1.3.9. Derive the Tarski-Bernays-Wajsberg axioms from Meredith's First CO Axiom

1. merco1
2. merco1lem1
3. retbwax4
4. retbwax2
5. merco1lem2
6. merco1lem3
7. merco1lem4
8. merco1lem5
9. merco1lem6
10. merco1lem7
11. retbwax3
12. merco1lem8
13. merco1lem9
14. merco1lem10
15. merco1lem11
16. merco1lem12
17. merco1lem13
18. merco1lem14
19. merco1lem15
20. merco1lem16
21. merco1lem17
22. merco1lem18
23. retbwax1