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