Theorem luk-1 658

Description: 1 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.

Assertion

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

Proof of Theorem luk-1

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

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  luklem1 661  luklem2 662  luklem4 664  luklem6 666  luklem7 667  luklem8 668

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org