con3ALT

Description: Proof of con3 from its associated inference con3i that illustrates the use of the weak deduction theorem dedt . (Contributed by NM, 27-Jun-2002) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019) Revised dedt and elimh . (Revised by Steven Nguyen, 27-Apr-2023) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	con3ALT	$⊢ (φ \to ψ) \to (\neg ψ \to \neg φ)$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ (if- ((φ \to ψ), ψ, φ) \leftrightarrow ψ) \to (if- ((φ \to ψ), ψ, φ) \leftrightarrow ψ)$
2	1	notbid	$⊢ (if- ((φ \to ψ), ψ, φ) \leftrightarrow ψ) \to (\neg if- ((φ \to ψ), ψ, φ) \leftrightarrow \neg ψ)$
3	2	imbi1d	$⊢ (if- ((φ \to ψ), ψ, φ) \leftrightarrow ψ) \to ((\neg if- ((φ \to ψ), ψ, φ) \to \neg φ) \leftrightarrow (\neg ψ \to \neg φ))$
4		imbi2	$⊢ (if- ((φ \to ψ), ψ, φ) \leftrightarrow ψ) \to ((φ \to if- ((φ \to ψ), ψ, φ)) \leftrightarrow (φ \to ψ))$
5		imbi2	$⊢ (if- ((φ \to ψ), ψ, φ) \leftrightarrow φ) \to ((φ \to if- ((φ \to ψ), ψ, φ)) \leftrightarrow (φ \to φ))$
6		id	$⊢ φ \to φ$
7	4 5 6	elimh	$⊢ φ \to if- ((φ \to ψ), ψ, φ)$
8	7	con3i	$⊢ \neg if- ((φ \to ψ), ψ, φ) \to \neg φ$
9	3 8	dedt	$⊢ (φ \to ψ) \to (\neg ψ \to \neg φ)$

Metamath Proof Explorer

Theorem con3ALT

Proof