 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 33041
 Description: Curry's axiom (a non-intuitionistic statement sometimes called a paradox of material implication) implies Peirce's axiom peirce 194 over minimal implicational calculus and the axiomatic definition of disjunction (olc 895, orc 894, jao 984). A shorter proof from bj-orim2 33039, pm1.2 928, syl6com 37 is possible if we accept to use pm1.2 928, itself a direct consequence of jao 984. (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 olc 895 . . 3 (𝜑 → (𝜑𝜑))
21imim2i 16 . . 3 (((𝜑𝜓) → 𝜑) → ((𝜑𝜓) → (𝜑𝜑)))
3 jao 984 . . 3 ((𝜑 → (𝜑𝜑)) → (((𝜑𝜓) → (𝜑𝜑)) → ((𝜑 ∨ (𝜑𝜓)) → (𝜑𝜑))))
41, 2, 3mpsyl 68 . 2 (((𝜑𝜓) → 𝜑) → ((𝜑 ∨ (𝜑𝜓)) → (𝜑𝜑)))
5 id 22 . . 3 (𝜑𝜑)
6 jao 984 . . 3 ((𝜑𝜑) → ((𝜑𝜑) → ((𝜑𝜑) → 𝜑)))
75, 5, 6mp2 9 . 2 ((𝜑𝜑) → 𝜑)
84, 7syl6com 37 1 ((𝜑 ∨ (𝜑𝜓)) → (((𝜑𝜓) → 𝜑) → 𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 874 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 199  df-an 386  df-or 875 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator