re1luk3

This theorem, along with re1luk1 and re1luk2 proves that tbw-ax1 , tbw-ax2 , tbw-ax3 , and tbw-ax4 , with ax-mp can be used as a complete axiom system for all of propositional calculus. (Contributed by Anthony Hart, 16-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	re1luk3	$⊢ φ \to (\neg φ \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		tbw-ax4	$⊢ ⊥ \to ψ$
2		tbw-ax1	$⊢ (φ \to ⊥) \to ((⊥ \to ψ) \to (φ \to ψ))$
3		tbwlem1	$⊢ ((φ \to ⊥) \to ((⊥ \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 ⊥) \to (φ \to ψ)$
6		tbwlem1	$⊢ ((φ \to ⊥) \to (φ \to ψ)) \to (φ \to ((φ \to ⊥) \to ψ))$
7	5 6	ax-mp	$⊢ φ \to ((φ \to ⊥) \to ψ)$
8		tbw-negdf	$⊢ ((\neg φ \to (φ \to ⊥)) \to (((φ \to ⊥) \to \neg φ) \to ⊥)) \to ⊥$
9		tbwlem5	$⊢ (((\neg φ \to (φ \to ⊥)) \to (((φ \to ⊥) \to \neg φ) \to ⊥)) \to ⊥) \to (\neg φ \to (φ \to ⊥))$
10	8 9	ax-mp	$⊢ \neg φ \to (φ \to ⊥)$
11		tbw-ax1	$⊢ (\neg φ \to (φ \to ⊥)) \to (((φ \to ⊥) \to ψ) \to (\neg φ \to ψ))$
12	10 11	ax-mp	$⊢ ((φ \to ⊥) \to ψ) \to (\neg φ \to ψ)$
13	7 12	tbwsyl	$⊢ φ \to (\neg φ \to ψ)$

Metamath Proof Explorer

Theorem re1luk3

Proof