Metamath Proof Explorer

Theorem wl-luk-pm2.27

Description: This theorem, called "Assertion", can be thought of as closed form of modus ponens ax-mp . Theorem *2.27 of WhiteheadRussell p. 104. Copy of pm2.27 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	wl-luk-pm2.27	$⊢ φ \to ((φ \to ψ) \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		wl-luk-ax1	$⊢ φ \to (\neg ψ \to φ)$
2		ax-luk1	$⊢ (\neg ψ \to φ) \to ((φ \to ψ) \to (\neg ψ \to ψ))$
3	1 2	wl-luk-syl	$⊢ φ \to ((φ \to ψ) \to (\neg ψ \to ψ))$
4		ax-luk2	$⊢ (\neg ψ \to ψ) \to ψ$
5	3 4	wl-luk-imtrdi	$⊢ φ \to ((φ \to ψ) \to ψ)$