![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.24 | GIF version |
Description: Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
Ref | Expression |
---|---|
pm2.24 | ⊢ (𝜑 → (¬ 𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21 618 | . 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | |
2 | 1 | com12 30 | 1 ⊢ (𝜑 → (¬ 𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in2 616 |
This theorem is referenced by: pm2.24d 623 pm2.53 723 pm2.82 813 pm4.81dc 909 dedlema 971 alexim 1656 eqneqall 2370 elnelall 2467 sotritric 4342 ltxrlt 8054 zltnle 9330 elfzonlteqm1 10242 qltnle 10278 hashfzp1 10839 dfgcd2 12050 oddprmdvds 12389 bj-fast 14971 nnnotnotr 15220 |
Copyright terms: Public domain | W3C validator |