Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-currypeirce Structured version   Visualization version   GIF version

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

Proof of Theorem bj-currypeirce
StepHypRef Expression
1 ax-1 6 . 2 (𝜑 → (((𝜑𝜓) → 𝜑) → 𝜑))
2 pm2.27 42 . 2 ((𝜑𝜓) → (((𝜑𝜓) → 𝜑) → 𝜑))
31, 2jaoi 864 1 ((𝜑 ∨ (𝜑𝜓)) → (((𝜑𝜓) → 𝜑) → 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 854
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 209  df-or 855
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator