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

Theorem bj-peircestab 33876
 Description: Over minimal implicational calculus, Peirce's law implies the double negation of the stability of any proposition (that is the interpretation when ⊥ is substitued for 𝜓). (Contributed by BJ, 30-Nov-2023.) (Proof modification is discouraged.)
Assertion
Ref Expression
bj-peircestab (((((𝜑𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜓)

Proof of Theorem bj-peircestab
StepHypRef Expression
1 id 22 . . . 4 (((((𝜑𝜓) → 𝜓) → 𝜑) → 𝜓) → ((((𝜑𝜓) → 𝜓) → 𝜑) → 𝜓))
21a2i 14 . . 3 ((((((𝜑𝜓) → 𝜓) → 𝜑) → 𝜓) → (((𝜑𝜓) → 𝜓) → 𝜑)) → (((((𝜑𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜓))
3 ax-1 6 . . . . . . 7 (𝜓 → ((𝜑𝜓) → 𝜓))
43imim2i 16 . . . . . 6 (((((𝜑𝜓) → 𝜓) → 𝜑) → 𝜓) → ((((𝜑𝜓) → 𝜓) → 𝜑) → ((𝜑𝜓) → 𝜓)))
5 peirce 204 . . . . . 6 (((((𝜑𝜓) → 𝜓) → 𝜑) → ((𝜑𝜓) → 𝜓)) → ((𝜑𝜓) → 𝜓))
64, 5syl 17 . . . . 5 (((((𝜑𝜓) → 𝜓) → 𝜑) → 𝜓) → ((𝜑𝜓) → 𝜓))
7 imim2 58 . . . . 5 ((𝜓𝜑) → (((𝜑𝜓) → 𝜓) → ((𝜑𝜓) → 𝜑)))
8 peirce 204 . . . . 5 (((𝜑𝜓) → 𝜑) → 𝜑)
96, 7, 8syl56 36 . . . 4 ((𝜓𝜑) → (((((𝜑𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜑))
109a1dd 50 . . 3 ((𝜓𝜑) → (((((𝜑𝜓) → 𝜓) → 𝜑) → 𝜓) → (((𝜑𝜓) → 𝜓) → 𝜑)))
112, 10syl11 33 . 2 (((((𝜑𝜓) → 𝜓) → 𝜑) → 𝜓) → ((𝜓𝜑) → 𝜓))
12 peirce 204 . 2 (((𝜓𝜑) → 𝜓) → 𝜓)
1311, 12syl 17 1 (((((𝜑𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator