Theorem retbwax1 1568

Description: tbw-ax1 1533 rederived from merco1 1546.

This theorem, along with retbwax2 1549, retbwax3 1556, and retbwax4 1548, shows that merco1 1546 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 1567	. . 3
2		merco1lem16 1565	. . 3
3	1, 2	ax-mp 5	. 2
4		merco1lem15 1564	. . . . . 6
5		merco1lem15 1564	. . . . . 6
6	4, 5	ax-mp 5	. . . . 5
7		merco1lem18 1567	. . . . 5
8	6, 7	ax-mp 5	. . . 4
9		merco1lem14 1563	. . . 4
10	8, 9	ax-mp 5	. . 3
11		merco1lem14 1563	. . . . . 6
12		merco1lem10 1559	. . . . . . . . 9
13		merco1 1546	. . . . . . . . 9
14	12, 13	ax-mp 5	. . . . . . . 8
15		merco1 1546	. . . . . . . 8
16	14, 15	ax-mp 5	. . . . . . 7
17		merco1 1546	. . . . . . 7
18	16, 17	ax-mp 5	. . . . . 6
19	11, 18	ax-mp 5	. . . . 5
20		merco1lem15 1564	. . . . 5
21	19, 20	ax-mp 5	. . . 4
22		merco1lem10 1559	. . . . . 6
23		merco1lem9 1558	. . . . . 6
24	22, 23	ax-mp 5	. . . . 5
25		merco1lem13 1562	. . . . 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

Syntax hints:  ->wi 4  wfal 1400

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 185  df-tru 1398  df-fal 1401