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 606 | . 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 604 |
This theorem is referenced by: pm2.24d 611 pm2.53 711 pm2.82 801 pm4.81dc 893 dedlema 953 alexim 1624 eqneqall 2318 elnelall 2415 sotritric 4246 ltxrlt 7830 zltnle 9100 elfzonlteqm1 9987 qltnle 10023 hashfzp1 10570 dfgcd2 11702 bj-fast 12952 |
Copyright terms: Public domain | W3C validator |