Theorem bj-currypeirce 36867

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

Assertion

Ref	Expression
bj-currypeirce	⊢ ((𝜑 ∨ (𝜑 → 𝜓)) → (((𝜑 → 𝜓) → 𝜑) → 𝜑))

Proof of Theorem bj-currypeirce

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 ⊢ (𝜑 → (((𝜑 → 𝜓) → 𝜑) → 𝜑))
2		pm2.27 42	. 2 ⊢ ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜑) → 𝜑))
3	1, 2	jaoi 863	1 ⊢ ((𝜑 ∨ (𝜑 → 𝜓)) → (((𝜑 → 𝜓) → 𝜑) → 𝜑))

Syntax hints:   → wi 4   ∨ wo 853

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

This theorem depends on definitions:  df-bi 208  df-or 854

This theorem is referenced by: (None)