Theorem luk-1 1420

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.)

Assertion

Ref	Expression
luk-1	⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ)))

Proof of Theorem luk-1

Step	Hyp	Ref	Expression
1		ax-meredith 1406	. 2 ⊢ (((((χ → χ) → (¬ ¬ ¬ φ → ¬ φ)) → ¬ ¬ φ) → ψ) → ((ψ → χ) → (φ → χ)))
2		merlem13 1419	. . . 4 ⊢ ((φ → ψ) → ((((χ → χ) → (¬ ¬ ¬ φ → ¬ φ)) → ¬ ¬ φ) → ψ))
3		merlem13 1419	. . . 4 ⊢ (((φ → ψ) → ((((χ → χ) → (¬ ¬ ¬ φ → ¬ φ)) → ¬ ¬ φ) → ψ)) → ((((((ψ → χ) → (φ → χ)) → φ) → (¬ ¬ ¬ (φ → ψ) → ¬ (φ → ψ))) → ¬ ¬ (φ → ψ)) → ((((χ → χ) → (¬ ¬ ¬ φ → ¬ φ)) → ¬ ¬ φ) → ψ)))
4	2, 3	ax-mp 5	. . 3 ⊢ ((((((ψ → χ) → (φ → χ)) → φ) → (¬ ¬ ¬ (φ → ψ) → ¬ (φ → ψ))) → ¬ ¬ (φ → ψ)) → ((((χ → χ) → (¬ ¬ ¬ φ → ¬ φ)) → ¬ ¬ φ) → ψ))
5		ax-meredith 1406	. . 3 ⊢ (((((((ψ → χ) → (φ → χ)) → φ) → (¬ ¬ ¬ (φ → ψ) → ¬ (φ → ψ))) → ¬ ¬ (φ → ψ)) → ((((χ → χ) → (¬ ¬ ¬ φ → ¬ φ)) → ¬ ¬ φ) → ψ)) → ((((((χ → χ) → (¬ ¬ ¬ φ → ¬ φ)) → ¬ ¬ φ) → ψ) → ((ψ → χ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))
6	4, 5	ax-mp 5	. 2 ⊢ ((((((χ → χ) → (¬ ¬ ¬ φ → ¬ φ)) → ¬ ¬ φ) → ψ) → ((ψ → χ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))
7	1, 6	ax-mp 5	1 ⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-meredith 1406

This theorem is used by:  luklem1  1423  luklem2  1424  luklem4  1426  luklem6  1428  luklem7  1429  luklem8  1430