retbwax1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > retbwax1		Structured version Visualization version Unicode version

Theorem retbwax1 1660

Description: tbw-ax1 1625 rederived from merco1 1638.

This theorem, along with retbwax2 1641, retbwax3 1648, and retbwax4 1640, shows that merco1 1638 with ax-mp 5 can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

**Assertion**
Ref	Expression
retbwax1

**Proof of Theorem retbwax1**
Step	Hyp	Ref	Expression
1		merco1lem18 1659	. . 3
2		merco1lem16 1657	. . 3
3	1, 2	ax-mp 5	. 2
4		merco1lem15 1656	. . . . . 6
5		merco1lem15 1656	. . . . . 6
6	4, 5	ax-mp 5	. . . . 5
7		merco1lem18 1659	. . . . 5
8	6, 7	ax-mp 5	. . . 4
9		merco1lem14 1655	. . . 4
10	8, 9	ax-mp 5	. . 3
11		merco1lem14 1655	. . . . . 6
12		merco1lem10 1651	. . . . . . . . 9
13		merco1 1638	. . . . . . . . 9
14	12, 13	ax-mp 5	. . . . . . . 8
15		merco1 1638	. . . . . . . 8
16	14, 15	ax-mp 5	. . . . . . 7
17		merco1 1638	. . . . . . 7
18	16, 17	ax-mp 5	. . . . . 6
19	11, 18	ax-mp 5	. . . . 5
20		merco1lem15 1656	. . . . 5
21	19, 20	ax-mp 5	. . . 4
22		merco1lem10 1651	. . . . . 6
23		merco1lem9 1650	. . . . . 6
24	22, 23	ax-mp 5	. . . . 5
25		merco1lem13 1654	. . . . 5
26	24, 25	ax-mp 5	. . . 4
27	21, 26	ax-mp 5	. . 3
28	10, 27	ax-mp 5	. 2
29	3, 28	ax-mp 5	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wfal 1488

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

This theorem depends on definitions: df-bi 197 df-tru 1486 df-fal 1489

This theorem is referenced by: (None)

W3C validator