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

Metamath Proof Explorer

Theorem re1luk3

Proof