Metamath Proof Explorer

Theorem wl-luk-ax2

Description: ax-2 proved from Lukasiewicz's axioms. (Contributed by Wolf Lammen, 17-Dec-2018) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	wl-luk-ax2	$⊢ (φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ))$

Proof

Step	Hyp	Ref	Expression
1		wl-luk-pm2.21	$⊢ \neg φ \to (φ \to χ)$
2	1	wl-luk-a1d	$⊢ \neg φ \to ((φ \to ψ) \to (φ \to χ))$
3		wl-luk-imim2	$⊢ (ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))$
4	2 3	wl-luk-ja	$⊢ (φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ))$