Theorem re1tbw4 1752

Description: tbw-ax4 1707 rederived from merco2 1740.

This theorem, along with re1tbw1 1749, re1tbw2 1750, and re1tbw3 1751, shows that merco2 1740, 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	⊢ (⊥ → 𝜑)

Proof of Theorem re1tbw4

Step	Hyp	Ref	Expression
1		re1tbw3 1751	. . 3 ⊢ (((𝜑 → 𝜑) → 𝜑) → 𝜑)
2		re1tbw2 1750	. . . 4 ⊢ (𝜑 → ((𝜑 → 𝜑) → 𝜑))
3		re1tbw1 1749	. . . 4 ⊢ ((𝜑 → ((𝜑 → 𝜑) → 𝜑)) → ((((𝜑 → 𝜑) → 𝜑) → 𝜑) → (𝜑 → 𝜑)))
4	2, 3	ax-mp 5	. . 3 ⊢ ((((𝜑 → 𝜑) → 𝜑) → 𝜑) → (𝜑 → 𝜑))
5	1, 4	ax-mp 5	. 2 ⊢ (𝜑 → 𝜑)
6		re1tbw3 1751	. . . . 5 ⊢ ((((⊥ → 𝜑) → 𝜑) → (⊥ → 𝜑)) → (⊥ → 𝜑))
7		re1tbw2 1750	. . . . . 6 ⊢ ((⊥ → 𝜑) → (((⊥ → 𝜑) → 𝜑) → (⊥ → 𝜑)))
8		re1tbw1 1749	. . . . . 6 ⊢ (((⊥ → 𝜑) → (((⊥ → 𝜑) → 𝜑) → (⊥ → 𝜑))) → (((((⊥ → 𝜑) → 𝜑) → (⊥ → 𝜑)) → (⊥ → 𝜑)) → ((⊥ → 𝜑) → (⊥ → 𝜑))))
9	7, 8	ax-mp 5	. . . . 5 ⊢ (((((⊥ → 𝜑) → 𝜑) → (⊥ → 𝜑)) → (⊥ → 𝜑)) → ((⊥ → 𝜑) → (⊥ → 𝜑)))
10	6, 9	ax-mp 5	. . . 4 ⊢ ((⊥ → 𝜑) → (⊥ → 𝜑))
11		mercolem3 1743	. . . . 5 ⊢ (((⊥ → 𝜑) → 𝜑) → ((⊥ → 𝜑) → (⊥ → 𝜑)))
12		merco2 1740	. . . . 5 ⊢ ((((⊥ → 𝜑) → 𝜑) → ((⊥ → 𝜑) → (⊥ → 𝜑))) → (((⊥ → 𝜑) → (⊥ → 𝜑)) → ((𝜑 → 𝜑) → ((𝜑 → 𝜑) → (⊥ → 𝜑)))))
13	11, 12	ax-mp 5	. . . 4 ⊢ (((⊥ → 𝜑) → (⊥ → 𝜑)) → ((𝜑 → 𝜑) → ((𝜑 → 𝜑) → (⊥ → 𝜑))))
14	10, 13	ax-mp 5	. . 3 ⊢ ((𝜑 → 𝜑) → ((𝜑 → 𝜑) → (⊥ → 𝜑)))
15	5, 14	ax-mp 5	. 2 ⊢ ((𝜑 → 𝜑) → (⊥ → 𝜑))
16	5, 15	ax-mp 5	1 ⊢ (⊥ → 𝜑)

Syntax hints:   → wi 4  ⊥wfal 1551

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 206  df-tru 1542  df-fal 1552

This theorem is referenced by: (None)