Users' Mathboxes 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 34371
Description: Over minimal implicational calculus, Peirce's law implies the double negation of the stability of any formula (that is the interpretation when is substituted for 𝜓 and for 𝜒). Therefore, the double negation of the stability of any formula is provable in classical refutability calculus. It is also provable in intuitionistic calculus (see iset.mm/bj-nnst) but it is not provable in minimal calculus (see bj-stabpeirce 34372). (Contributed by BJ, 30-Nov-2023.) Axiom ax-3 8 is only used through Peirce's law peirce 205. (Proof modification is discouraged.)
Assertion
Ref Expression
bj-peircestab (((((𝜑𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜒)

Proof of Theorem bj-peircestab
StepHypRef Expression
1 bj-nnclav 34364 . . 3 ((((((𝜑𝜓) → 𝜒) → 𝜑) → 𝜒) → (((𝜑𝜓) → 𝜒) → 𝜑)) → (((((𝜑𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜒))
2 ax-1 6 . . . . . . 7 (𝜒 → ((𝜑𝜓) → 𝜒))
32imim2i 16 . . . . . 6 (((((𝜑𝜓) → 𝜒) → 𝜑) → 𝜒) → ((((𝜑𝜓) → 𝜒) → 𝜑) → ((𝜑𝜓) → 𝜒)))
4 peirce 205 . . . . . 6 (((((𝜑𝜓) → 𝜒) → 𝜑) → ((𝜑𝜓) → 𝜒)) → ((𝜑𝜓) → 𝜒))
53, 4syl 17 . . . . 5 (((((𝜑𝜓) → 𝜒) → 𝜑) → 𝜒) → ((𝜑𝜓) → 𝜒))
6 imim2 58 . . . . 5 ((𝜒𝜑) → (((𝜑𝜓) → 𝜒) → ((𝜑𝜓) → 𝜑)))
7 peirce 205 . . . . 5 (((𝜑𝜓) → 𝜑) → 𝜑)
85, 6, 7syl56 36 . . . 4 ((𝜒𝜑) → (((((𝜑𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜑))
98a1dd 50 . . 3 ((𝜒𝜑) → (((((𝜑𝜓) → 𝜒) → 𝜑) → 𝜒) → (((𝜑𝜓) → 𝜒) → 𝜑)))
101, 9syl11 33 . 2 (((((𝜑𝜓) → 𝜒) → 𝜑) → 𝜒) → ((𝜒𝜑) → 𝜒))
11 peirce 205 . 2 (((𝜒𝜑) → 𝜒) → 𝜒)
1210, 11syl 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