Metamath Proof Explorer

Theorem tbwlem3

Description: Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	tbwlem3	$⊢ ((((φ \to ⊥) \to φ) \to φ) \to ψ) \to ψ$

Proof

Step	Hyp	Ref	Expression
1		tbw-ax3	$⊢ ((φ \to ⊥) \to φ) \to φ$
2		tbw-ax2	$⊢ (((φ \to ⊥) \to φ) \to φ) \to (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to (((φ \to ⊥) \to φ) \to φ))$
3		tbw-ax1	$⊢ (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to (((φ \to ⊥) \to φ) \to φ)) \to (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to ψ))$
4	2 3	tbwsyl	$⊢ (((φ \to ⊥) \to φ) \to φ) \to (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to ψ))$
5	1 4	ax-mp	$⊢ ((((φ \to ⊥) \to φ) \to φ) \to ψ) \to (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to ψ)$
6		tbw-ax1	$⊢ (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to ψ)) \to (((((((φ \to ⊥) \to φ) \to φ) \to ψ) \to ψ) \to ψ) \to (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to ψ))$
7		tbw-ax3	$⊢ (((((((φ \to ⊥) \to φ) \to φ) \to ψ) \to ψ) \to ψ) \to (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to ψ)) \to (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to ψ)$
8	6 7	tbwsyl	$⊢ (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to ψ)) \to (((((φ \to ⊥) \to φ) \to φ) \to ψ) \to ψ)$
9	5 8	ax-mp	$⊢ ((((φ \to ⊥) \to φ) \to φ) \to ψ) \to ψ$