This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem luk-1

Description: 1 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom. (Contributed by NM, 14-Dec-2002) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		meredith	$⊢ ((((χ \to χ) \to (\neg \neg \neg φ \to \neg φ)) \to \neg \neg φ) \to ψ) \to ((ψ \to χ) \to (φ \to χ))$
2		merlem13	$⊢ (φ \to ψ) \to ((((χ \to χ) \to (\neg \neg \neg φ \to \neg φ)) \to \neg \neg φ) \to ψ)$
3		merlem13	$⊢ ((φ \to ψ) \to ((((χ \to χ) \to (\neg \neg \neg φ \to \neg φ)) \to \neg \neg φ) \to ψ)) \to ((((((ψ \to χ) \to (φ \to χ)) \to φ) \to (\neg \neg \neg (φ \to ψ) \to \neg (φ \to ψ))) \to \neg \neg (φ \to ψ)) \to ((((χ \to χ) \to (\neg \neg \neg φ \to \neg φ)) \to \neg \neg φ) \to ψ))$
4	2 3	ax-mp	$⊢ (((((ψ \to χ) \to (φ \to χ)) \to φ) \to (\neg \neg \neg (φ \to ψ) \to \neg (φ \to ψ))) \to \neg \neg (φ \to ψ)) \to ((((χ \to χ) \to (\neg \neg \neg φ \to \neg φ)) \to \neg \neg φ) \to ψ)$
5		meredith	$⊢ ((((((ψ \to χ) \to (φ \to χ)) \to φ) \to (\neg \neg \neg (φ \to ψ) \to \neg (φ \to ψ))) \to \neg \neg (φ \to ψ)) \to ((((χ \to χ) \to (\neg \neg \neg φ \to \neg φ)) \to \neg \neg φ) \to ψ)) \to ((((((χ \to χ) \to (\neg \neg \neg φ \to \neg φ)) \to \neg \neg φ) \to ψ) \to ((ψ \to χ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))$
6	4 5	ax-mp	$⊢ (((((χ \to χ) \to (\neg \neg \neg φ \to \neg φ)) \to \neg \neg φ) \to ψ) \to ((ψ \to χ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))$
7	1 6	ax-mp	$⊢ (φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))$