Theorem re1tbw4 1513

Description: tbw-ax4 1468 rederived from merco2 1501.

This theorem, along with re1tbw1 1510, re1tbw2 1511, and re1tbw3 1512, shows that merco2 1501, along with ax-mp 5, can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
re1tbw4	|- ( F. -> ph)

Proof of Theorem re1tbw4

Step	Hyp	Ref	Expression
1		re1tbw3 1512	. . 3 |- (((ph -> ph) -> ph) -> ph)
2		re1tbw2 1511	. . . 4 |- (ph -> ((ph -> ph) -> ph))
3		re1tbw1 1510	. . . 4 |- ((ph -> ((ph -> ph) -> ph)) -> ((((ph -> ph) -> ph) -> ph) -> (ph -> ph)))
4	2, 3	ax-mp 5	. . 3 |- ((((ph -> ph) -> ph) -> ph) -> (ph -> ph))
5	1, 4	ax-mp 5	. 2 |- (ph -> ph)
6		re1tbw3 1512	. . . . 5 |- (((( F. -> ph) -> ph) -> ( F. -> ph)) -> ( F. -> ph))
7		re1tbw2 1511	. . . . . 6 |- (( F. -> ph) -> ((( F. -> ph) -> ph) -> ( F. -> ph)))
8		re1tbw1 1510	. . . . . 6 |- ((( F. -> ph) -> ((( F. -> ph) -> ph) -> ( F. -> ph))) -> ((((( F. -> ph) -> ph) -> ( F. -> ph)) -> ( F. -> ph)) -> (( F. -> ph) -> ( F. -> ph))))
9	7, 8	ax-mp 5	. . . . 5 |- ((((( F. -> ph) -> ph) -> ( F. -> ph)) -> ( F. -> ph)) -> (( F. -> ph) -> ( F. -> ph)))
10	6, 9	ax-mp 5	. . . 4 |- (( F. -> ph) -> ( F. -> ph))
11		mercolem3 1504	. . . . 5 |- ((( F. -> ph) -> ph) -> (( F. -> ph) -> ( F. -> ph)))
12		merco2 1501	. . . . 5 |- (((( F. -> ph) -> ph) -> (( F. -> ph) -> ( F. -> ph))) -> ((( F. -> ph) -> ( F. -> ph)) -> ((ph -> ph) -> ((ph -> ph) -> ( F. -> ph)))))
13	11, 12	ax-mp 5	. . . 4 |- ((( F. -> ph) -> ( F. -> ph)) -> ((ph -> ph) -> ((ph -> ph) -> ( F. -> ph))))
14	10, 13	ax-mp 5	. . 3 |- ((ph -> ph) -> ((ph -> ph) -> ( F. -> ph)))
15	5, 14	ax-mp 5	. 2 |- ((ph -> ph) -> ( F. -> ph))
16	5, 15	ax-mp 5	1 |- ( F. -> ph)

Syntax hints:   -> wi 4   F. wfal 1317

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 177  df-tru 1319  df-fal 1320

This theorem is referenced by: (None)