![]() |
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 589 | . 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-1 5 ax-2 6 ax-mp 7 ax-in2 587 |
This theorem is referenced by: pm2.24d 594 pm2.53 694 pm2.82 784 pm4.81dc 876 dedlema 936 alexim 1607 eqneqall 2292 elnelall 2389 sotritric 4206 ltxrlt 7754 zltnle 9004 elfzonlteqm1 9880 qltnle 9916 hashfzp1 10463 dfgcd2 11548 bj-fast 12645 |
Copyright terms: Public domain | W3C validator |