Theorem bj-stabpeirce 37172

Description: This minimal implicational calculus tautology is used in the following argument: When 𝜑, 𝜓, 𝜒, 𝜃, 𝜏 are replaced respectively by (𝜑 → ⊥), ⊥, 𝜑, ⊥, ⊥, the antecedent becomes ¬ ¬ (¬ ¬ 𝜑 → 𝜑), that is, the double negation of the stability of 𝜑. If that statement were provable in minimal calculus, then, since ⊥ plays no particular role in minimal calculus, also the statement with 𝜓 in place of ⊥ would be provable. The corresponding consequent is (((𝜓 → 𝜑) → 𝜓) → 𝜓), that is, the non-intuitionistic Peirce law. Therefore, the double negation of the stability of any formula is not provable in minimal calculus. However, it is provable both in intuitionistic calculus (see iset.mm/bj-nnst) and in classical refutability calculus (see bj-peircestab 37171). (Contributed by BJ, 30-Nov-2023.) (Revised by BJ, 30-Jul-2024.) (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-stabpeirce	⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜃) → 𝜏) → (((𝜓 → 𝜒) → 𝜃) → 𝜏))

Proof of Theorem bj-stabpeirce

Step	Hyp	Ref	Expression
1		jarr 107	. . 3 ⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒))
2	1	imim1i 64	. 2 ⊢ (((𝜓 → 𝜒) → 𝜃) → (((𝜑 → 𝜓) → 𝜒) → 𝜃))
3	2	imim1i 64	1 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜃) → 𝜏) → (((𝜓 → 𝜒) → 𝜃) → 𝜏))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by: (None)