Metamath Proof Explorer

Theorem bj-currypeirce

Description: Curry's axiom curryax (a non-intuitionistic positive statement sometimes called a paradox of material implication) implies Peirce's axiom peirce over minimal implicational calculus and the axiomatic definition of disjunction (actually, only the elimination axiom jao via its inference form jaoi ; the introduction axioms olc and orc are not needed). Note that this theorem shows that actually, the standard instance of curryax implies the standard instance of peirce , which is not the case for the converse bj-peircecurry . (Contributed by BJ, 15-Jun-2021) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	bj-currypeirce	$⊢ (φ \lor (φ \to ψ)) \to (((φ \to ψ) \to φ) \to φ)$

Proof

Step	Hyp	Ref	Expression
1		ax-1	$⊢ φ \to (((φ \to ψ) \to φ) \to φ)$
2		pm2.27	$⊢ (φ \to ψ) \to (((φ \to ψ) \to φ) \to φ)$
3	1 2	jaoi	$⊢ (φ \lor (φ \to ψ)) \to (((φ \to ψ) \to φ) \to φ)$