![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm3.2im | GIF version |
Description: In classical logic, this is just a restatement of pm3.2 138. In intuitionistic logic, it still holds, but is weaker than pm3.2. (Contributed by Mario Carneiro, 12-May-2015.) |
Ref | Expression |
---|---|
pm3.2im | ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.27 40 | . 2 ⊢ (𝜑 → ((𝜑 → ¬ 𝜓) → ¬ 𝜓)) | |
2 | 1 | con2d 592 | 1 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓))) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-in1 582 ax-in2 583 |
This theorem is referenced by: expi 605 jc 618 expt 621 imnan 662 dfandc 819 |
Copyright terms: Public domain | W3C validator |