| Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-currypeirce | Structured version Visualization version GIF version | ||
| Description: Curry's axiom curryax 904 (a non-intuitionistic positive statement sometimes called a paradox of material implication) implies Peirce's axiom peirce 204 over minimal implicational calculus and the axiomatic definition of disjunction (actually, only the elimination axiom jao 973 via its inference form jaoi 868; the introduction axioms olc 879 and orc 878 are not needed). Note that this theorem shows that actually, the standard instance of curryax 904 implies the standard instance of peirce 204, which is not the case for the converse bj-peircecurry 37000. (Contributed by BJ, 15-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| bj-currypeirce | ⊢ ((𝜑 ∨ (𝜑 → 𝜓)) → (((𝜑 → 𝜓) → 𝜑) → 𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-1 6 | . 2 ⊢ (𝜑 → (((𝜑 → 𝜓) → 𝜑) → 𝜑)) | |
| 2 | pm2.27 42 | . 2 ⊢ ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜑) → 𝜑)) | |
| 3 | 1, 2 | jaoi 868 | 1 ⊢ ((𝜑 ∨ (𝜑 → 𝜓)) → (((𝜑 → 𝜓) → 𝜑) → 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∨ wo 858 |
| 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 209 df-or 859 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |