Metamath Proof Explorer

Theorem frege32

Description: Deduce con1 from con3 . Proposition 32 of Frege1879 p. 44. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

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

Step	Hyp	Ref	Expression
1		ax-frege31	$⊢ \neg \neg φ \to φ$
2		frege7	$⊢ (\neg \neg φ \to φ) \to (((\neg φ \to ψ) \to (\neg ψ \to \neg \neg φ)) \to ((\neg φ \to ψ) \to (\neg ψ \to φ)))$
3	1 2	ax-mp	$⊢ ((\neg φ \to ψ) \to (\neg ψ \to \neg \neg φ)) \to ((\neg φ \to ψ) \to (\neg ψ \to φ))$