re1tbw4

This theorem, along with re1tbw1 , re1tbw2 , and re1tbw3 , shows that merco2 , along with ax-mp , 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.)

		Ref	Expression
	Assertion	re1tbw4	$⊢ ⊥ \to φ$

Proof

Step	Hyp	Ref	Expression
1		re1tbw3	$⊢ ((φ \to φ) \to φ) \to φ$
2		re1tbw2	$⊢ φ \to ((φ \to φ) \to φ)$
3		re1tbw1	$⊢ (φ \to ((φ \to φ) \to φ)) \to ((((φ \to φ) \to φ) \to φ) \to (φ \to φ))$
4	2 3	ax-mp	$⊢ (((φ \to φ) \to φ) \to φ) \to (φ \to φ)$
5	1 4	ax-mp	$⊢ φ \to φ$
6		re1tbw3	$⊢ (((⊥ \to φ) \to φ) \to (⊥ \to φ)) \to (⊥ \to φ)$
7		re1tbw2	$⊢ (⊥ \to φ) \to (((⊥ \to φ) \to φ) \to (⊥ \to φ))$
8		re1tbw1	$⊢ ((⊥ \to φ) \to (((⊥ \to φ) \to φ) \to (⊥ \to φ))) \to (((((⊥ \to φ) \to φ) \to (⊥ \to φ)) \to (⊥ \to φ)) \to ((⊥ \to φ) \to (⊥ \to φ)))$
9	7 8	ax-mp	$⊢ ((((⊥ \to φ) \to φ) \to (⊥ \to φ)) \to (⊥ \to φ)) \to ((⊥ \to φ) \to (⊥ \to φ))$
10	6 9	ax-mp	$⊢ (⊥ \to φ) \to (⊥ \to φ)$
11		mercolem3	$⊢ ((⊥ \to φ) \to φ) \to ((⊥ \to φ) \to (⊥ \to φ))$
12		merco2	$⊢ (((⊥ \to φ) \to φ) \to ((⊥ \to φ) \to (⊥ \to φ))) \to (((⊥ \to φ) \to (⊥ \to φ)) \to ((φ \to φ) \to ((φ \to φ) \to (⊥ \to φ))))$
13	11 12	ax-mp	$⊢ ((⊥ \to φ) \to (⊥ \to φ)) \to ((φ \to φ) \to ((φ \to φ) \to (⊥ \to φ)))$
14	10 13	ax-mp	$⊢ (φ \to φ) \to ((φ \to φ) \to (⊥ \to φ))$
15	5 14	ax-mp	$⊢ (φ \to φ) \to (⊥ \to φ)$
16	5 15	ax-mp	$⊢ ⊥ \to φ$

Metamath Proof Explorer

Theorem re1tbw4

Proof